Theorem elunii 4877

Description: Membership in class union. (Contributed by NM, 24-Mar-1995.)

Assertion

Ref	Expression
elunii	⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Proof of Theorem elunii

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2852	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2851	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 643	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3556	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 683	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4875	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 237	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∪ cuni 4872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-uni 4873

This theorem is referenced by:  ssuni  4898  unipw  5431  opeluu  5452  unon  7823  limuni3  7844  naddsuc2  8684  uniinqs  8791  trcl  9693  rankwflemb  9761  ac5num  10016  dfac3  10101  isf34lem4  10356  axcclem  10436  ttukeylem7  10494  brdom7disj  10510  brdom6disj  10511  wrdexb  14558  dprdfeq0  20089  unichnlidl  21362  ssdifidllem  21484  tgss2  23144  ppttop  23164  isclo  23244  neips  23270  2ndcomap  23615  2ndcsep  23616  locfincmp  23683  comppfsc  23689  txkgen  23809  txconn  23846  basqtop  23868  nrmr0reg  23906  alexsublem  24201  alexsubALTlem4  24207  alexsubALT  24208  ptcmplem4  24212  unirnblps  24576  unirnbl  24577  blbas  24587  met2ndci  24679  bndth  25117  dyadmbllem  25758  opnmbllem  25760  ssmxidllem  33756  dya2iocnei  34672  dstfrvunirn  34865  pconnconn  35723  cvmcov2  35767  cvmlift2lem11  35805  cvmlift2lem12  35806  neibastop2lem  36871  onint1  36960  ttcid  37003  ttctr  37004  dfttc2g  37017  icoreunrn  38005  opnmbllem0  38307  heibor1  38461  unichnidl  38682  prtlem16  39643  prter2  39655  truniALT  45250  unipwrVD  45540  unipwr  45541  truniALTVD  45586  unisnALT  45634  permaxun  45720  restuni3  45836  disjinfi  45910  stoweidlem43  46757  stoweidlem55  46769  salexct  47048