Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjprg Structured version   Unicode version

Theorem disjprg 4362
 Description: A pair collection is disjoint iff the two sets in the family have empty intersection. (Contributed by Mario Carneiro, 14-Nov-2016.)
Hypotheses
Ref Expression
disjprg.1
disjprg.2
Assertion
Ref Expression
disjprg Disj
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem disjprg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqeq1 2432 . . . . . . 7
2 nfcv 2569 . . . . . . . . . 10
3 nfcv 2569 . . . . . . . . . 10
4 disjprg.1 . . . . . . . . . 10
52, 3, 4csbhypf 3357 . . . . . . . . 9
65ineq1d 3606 . . . . . . . 8
76eqeq1d 2430 . . . . . . 7
81, 7orbi12d 714 . . . . . 6
98ralbidv 2804 . . . . 5
10 eqeq1 2432 . . . . . . 7
11 nfcv 2569 . . . . . . . . . 10
12 nfcv 2569 . . . . . . . . . 10
13 disjprg.2 . . . . . . . . . 10
1411, 12, 13csbhypf 3357 . . . . . . . . 9
1514ineq1d 3606 . . . . . . . 8
1615eqeq1d 2430 . . . . . . 7
1710, 16orbi12d 714 . . . . . 6
1817ralbidv 2804 . . . . 5
199, 18ralprg 3992 . . . 4
21 id 22 . . . . . . . . . 10
2221eqcomd 2434 . . . . . . . . 9
2322orcd 393 . . . . . . . 8
24 a1tru 1453 . . . . . . . 8
2523, 242thd 243 . . . . . . 7
26 eqeq2 2439 . . . . . . . 8
2711, 12, 13csbhypf 3357 . . . . . . . . . 10
2827ineq2d 3607 . . . . . . . . 9
2928eqeq1d 2430 . . . . . . . 8
3026, 29orbi12d 714 . . . . . . 7
3125, 30ralprg 3992 . . . . . 6
32313adant3 1025 . . . . 5
33 simp3 1007 . . . . . . . 8
3433neneqd 2606 . . . . . . 7
35 biorf 406 . . . . . . 7
3634, 35syl 17 . . . . . 6
37 tru 1441 . . . . . . 7
3837biantrur 508 . . . . . 6
3936, 38syl6bb 264 . . . . 5
4032, 39bitr4d 259 . . . 4
41 eqeq2 2439 . . . . . . . . 9
42 eqcom 2435 . . . . . . . . 9
4341, 42syl6bb 264 . . . . . . . 8
442, 3, 4csbhypf 3357 . . . . . . . . . . 11
4544ineq2d 3607 . . . . . . . . . 10
46 incom 3598 . . . . . . . . . 10
4745, 46syl6eq 2478 . . . . . . . . 9
4847eqeq1d 2430 . . . . . . . 8
4943, 48orbi12d 714 . . . . . . 7
50 id 22 . . . . . . . . . 10
5150eqcomd 2434 . . . . . . . . 9
5251orcd 393 . . . . . . . 8
53 a1tru 1453 . . . . . . . 8
5452, 532thd 243 . . . . . . 7
5549, 54ralprg 3992 . . . . . 6
56553adant3 1025 . . . . 5
5737biantru 507 . . . . . 6
5836, 57syl6bb 264 . . . . 5
5956, 58bitr4d 259 . . . 4
6040, 59anbi12d 715 . . 3
6120, 60bitrd 256 . 2
62 disjors 4352 . 2 Disj
63 pm4.24 647 . 2
6461, 62, 633bitr4g 291 1 Disj
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370   w3a 982   wceq 1437   wtru 1438   wcel 1872   wne 2599  wral 2714  csb 3338   cin 3378  c0 3704  cpr 3943  Disj wdisj 4337 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-nul 3705  df-sn 3942  df-pr 3944  df-disj 4338 This theorem is referenced by:  disjdifprg  28131  unelldsys  28932  pmeasmono  29109  probun  29204  meadjun  38151
 Copyright terms: Public domain W3C validator