Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  disjif2 Structured version   Visualization version   Unicode version

Theorem disjif2 28191
 Description: Property of a disjoint collection: if and have a common element , then . (Contributed by Thierry Arnoux, 6-Apr-2017.)
Hypotheses
Ref Expression
disjif2.1
disjif2.2
disjif2.3
Assertion
Ref Expression
disjif2 Disj
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem disjif2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inelcm 3819 . 2
2 disjif2.1 . . . . . . . 8
32disjorsf 28190 . . . . . . 7 Disj
4 equequ1 1867 . . . . . . . . 9
5 csbeq1 3366 . . . . . . . . . . . 12
6 csbid 3371 . . . . . . . . . . . 12
75, 6syl6eq 2501 . . . . . . . . . . 11
87ineq1d 3633 . . . . . . . . . 10
98eqeq1d 2453 . . . . . . . . 9
104, 9orbi12d 716 . . . . . . . 8
11 eqeq2 2462 . . . . . . . . 9
12 nfcv 2592 . . . . . . . . . . . 12
13 disjif2.2 . . . . . . . . . . . 12
14 disjif2.3 . . . . . . . . . . . 12
1512, 13, 14csbhypf 3382 . . . . . . . . . . 11
1615ineq2d 3634 . . . . . . . . . 10
1716eqeq1d 2453 . . . . . . . . 9
1811, 17orbi12d 716 . . . . . . . 8
1910, 18rspc2v 3159 . . . . . . 7
203, 19syl5bi 221 . . . . . 6 Disj
2120impcom 432 . . . . 5 Disj
2221ord 379 . . . 4 Disj
2322necon1ad 2641 . . 3 Disj
24233impia 1205 . 2 Disj
251, 24syl3an3 1303 1 Disj
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 370   wa 371   w3a 985   wceq 1444   wcel 1887  wnfc 2579   wne 2622  wral 2737  csb 3363   cin 3403  c0 3731  Disj wdisj 4373 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rmo 2745  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-in 3411  df-nul 3732  df-disj 4374 This theorem is referenced by:  disjabrexf  28193
 Copyright terms: Public domain W3C validator