Theorem elunii 4876

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 2817	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2816	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3563	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 671	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4874	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-uni 4872

This theorem is referenced by:  ssuni  4896  unipw  5410  opeluu  5430  unon  7806  limuni3  7828  naddsuc2  8665  uniinqs  8770  trcl  9681  rankwflemb  9746  ac5num  9989  dfac3  10074  isf34lem4  10330  axcclem  10410  ttukeylem7  10468  brdom7disj  10484  brdom6disj  10485  wrdexb  14490  dprdfeq0  19954  tgss2  22874  ppttop  22894  isclo  22974  neips  23000  2ndcomap  23345  2ndcsep  23346  locfincmp  23413  comppfsc  23419  txkgen  23539  txconn  23576  basqtop  23598  nrmr0reg  23636  alexsublem  23931  alexsubALTlem4  23937  alexsubALT  23938  ptcmplem4  23942  unirnblps  24307  unirnbl  24308  blbas  24318  met2ndci  24410  bndth  24857  dyadmbllem  25500  opnmbllem  25502  ssdifidllem  33427  ssmxidllem  33444  dya2iocnei  34273  dstfrvunirn  34466  pconnconn  35218  cvmcov2  35262  cvmlift2lem11  35300  cvmlift2lem12  35301  neibastop2lem  36348  onint1  36437  icoreunrn  37347  opnmbllem0  37650  heibor1  37804  unichnidl  38025  prtlem16  38862  prter2  38874  truniALT  44531  unipwrVD  44821  unipwr  44822  truniALTVD  44867  unisnALT  44915  permaxun  45001  restuni3  45112  disjinfi  45186  stoweidlem43  46041  stoweidlem55  46053  salexct  46332