Theorem elunii 4914

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 2823	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2822	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3588	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 670	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4912	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 233	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-uni 4910

This theorem is referenced by:  ssuni  4937  unipw  5451  opeluu  5471  unon  7819  limuni3  7841  uniinqs  8791  trcl  9723  rankwflemb  9788  ac5num  10031  dfac3  10116  isf34lem4  10372  axcclem  10452  ttukeylem7  10510  brdom7disj  10526  brdom6disj  10527  wrdexb  14475  dprdfeq0  19892  tgss2  22490  ppttop  22510  isclo  22591  neips  22617  2ndcomap  22962  2ndcsep  22963  locfincmp  23030  comppfsc  23036  txkgen  23156  txconn  23193  basqtop  23215  nrmr0reg  23253  alexsublem  23548  alexsubALTlem4  23554  alexsubALT  23555  ptcmplem4  23559  unirnblps  23925  unirnbl  23926  blbas  23936  met2ndci  24031  bndth  24474  dyadmbllem  25116  opnmbllem  25118  ssmxidllem  32620  dya2iocnei  33312  dstfrvunirn  33504  pconnconn  34253  cvmcov2  34297  cvmlift2lem11  34335  cvmlift2lem12  34336  neibastop2lem  35293  onint1  35382  icoreunrn  36288  opnmbllem0  36572  heibor1  36726  unichnidl  36947  prtlem16  37787  prter2  37799  naddsuc2  42191  truniALT  43350  unipwrVD  43641  unipwr  43642  truniALTVD  43687  unisnALT  43735  restuni3  43855  disjinfi  43939  stoweidlem43  44807  stoweidlem55  44819  salexct  45098