Theorem elunii 4888

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 3576	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 671	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4886	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-uni 4884

This theorem is referenced by:  ssuni  4908  unipw  5425  opeluu  5445  unon  7825  limuni3  7847  naddsuc2  8713  uniinqs  8811  trcl  9742  rankwflemb  9807  ac5num  10050  dfac3  10135  isf34lem4  10391  axcclem  10471  ttukeylem7  10529  brdom7disj  10545  brdom6disj  10546  wrdexb  14543  dprdfeq0  20005  tgss2  22925  ppttop  22945  isclo  23025  neips  23051  2ndcomap  23396  2ndcsep  23397  locfincmp  23464  comppfsc  23470  txkgen  23590  txconn  23627  basqtop  23649  nrmr0reg  23687  alexsublem  23982  alexsubALTlem4  23988  alexsubALT  23989  ptcmplem4  23993  unirnblps  24358  unirnbl  24359  blbas  24369  met2ndci  24461  bndth  24908  dyadmbllem  25552  opnmbllem  25554  ssdifidllem  33471  ssmxidllem  33488  dya2iocnei  34314  dstfrvunirn  34507  pconnconn  35253  cvmcov2  35297  cvmlift2lem11  35335  cvmlift2lem12  35336  neibastop2lem  36378  onint1  36467  icoreunrn  37377  opnmbllem0  37680  heibor1  37834  unichnidl  38055  prtlem16  38887  prter2  38899  truniALT  44566  unipwrVD  44856  unipwr  44857  truniALTVD  44902  unisnALT  44950  permaxun  45036  restuni3  45142  disjinfi  45216  stoweidlem43  46072  stoweidlem55  46084  salexct  46363