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

Theorem disjprg 4200
 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 2441 . . . . . . 7
2 nfcv 2571 . . . . . . . . . 10
3 nfcv 2571 . . . . . . . . . 10
4 disjprg.1 . . . . . . . . . 10
52, 3, 4csbhypf 3278 . . . . . . . . 9
65ineq1d 3533 . . . . . . . 8
76eqeq1d 2443 . . . . . . 7
81, 7orbi12d 691 . . . . . 6
98ralbidv 2717 . . . . 5
10 eqeq1 2441 . . . . . . 7
11 nfcv 2571 . . . . . . . . . 10
12 nfcv 2571 . . . . . . . . . 10
13 disjprg.2 . . . . . . . . . 10
1411, 12, 13csbhypf 3278 . . . . . . . . 9
1514ineq1d 3533 . . . . . . . 8
1615eqeq1d 2443 . . . . . . 7
1710, 16orbi12d 691 . . . . . 6
1817ralbidv 2717 . . . . 5
199, 18ralprg 3849 . . . 4
21 id 20 . . . . . . . . . 10
2221eqcomd 2440 . . . . . . . . 9
2322orcd 382 . . . . . . . 8
24 a1tru 1339 . . . . . . . 8
2523, 242thd 232 . . . . . . 7
26 eqeq2 2444 . . . . . . . 8
2711, 12, 13csbhypf 3278 . . . . . . . . . 10
2827ineq2d 3534 . . . . . . . . 9
2928eqeq1d 2443 . . . . . . . 8
3026, 29orbi12d 691 . . . . . . 7
3125, 30ralprg 3849 . . . . . 6
32313adant3 977 . . . . 5
33 simp3 959 . . . . . . . 8
3433neneqd 2614 . . . . . . 7
35 biorf 395 . . . . . . 7
3634, 35syl 16 . . . . . 6
37 tru 1330 . . . . . . 7
3837biantrur 493 . . . . . 6
3936, 38syl6bb 253 . . . . 5
4032, 39bitr4d 248 . . . 4
41 eqeq2 2444 . . . . . . . . 9
42 eqcom 2437 . . . . . . . . 9
4341, 42syl6bb 253 . . . . . . . 8
442, 3, 4csbhypf 3278 . . . . . . . . . . 11
4544ineq2d 3534 . . . . . . . . . 10
46 incom 3525 . . . . . . . . . 10
4745, 46syl6eq 2483 . . . . . . . . 9
4847eqeq1d 2443 . . . . . . . 8
4943, 48orbi12d 691 . . . . . . 7
50 id 20 . . . . . . . . . 10
5150eqcomd 2440 . . . . . . . . 9
5251orcd 382 . . . . . . . 8
53 a1tru 1339 . . . . . . . 8
5452, 532thd 232 . . . . . . 7
5549, 54ralprg 3849 . . . . . 6
56553adant3 977 . . . . 5
5737biantru 492 . . . . . 6
5836, 57syl6bb 253 . . . . 5
5956, 58bitr4d 248 . . . 4
6040, 59anbi12d 692 . . 3
6120, 60bitrd 245 . 2
62 disjors 4190 . 2 Disj
63 pm4.24 625 . 2
6461, 62, 633bitr4g 280 1 Disj
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   w3a 936   wtru 1325   wceq 1652   wcel 1725   wne 2598  wral 2697  csb 3243   cin 3311  c0 3620  cpr 3807  Disj wdisj 4174 This theorem is referenced by:  disjdifprg  24009  probun  24669 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-nul 3621  df-sn 3812  df-pr 3813  df-disj 4175
 Copyright terms: Public domain W3C validator