Theorem elunii 4845

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 2903	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2902	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3599	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 669	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4843	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 236	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-uni 4841

This theorem is referenced by:  ssuni  4865  unipw  5345  opeluu  5364  unon  7548  limuni3  7569  uniinqs  8379  trcl  9172  rankwflemb  9224  ac5num  9464  dfac3  9549  isf34lem4  9801  axcclem  9881  ttukeylem7  9939  brdom7disj  9955  brdom6disj  9956  wrdexb  13876  dprdfeq0  19146  tgss2  21597  ppttop  21617  isclo  21697  neips  21723  2ndcomap  22068  2ndcsep  22069  locfincmp  22136  comppfsc  22142  txkgen  22262  txconn  22299  basqtop  22321  nrmr0reg  22359  alexsublem  22654  alexsubALTlem4  22660  alexsubALT  22661  ptcmplem4  22665  unirnblps  23031  unirnbl  23032  blbas  23042  met2ndci  23134  bndth  23564  dyadmbllem  24202  opnmbllem  24204  ssmxidllem  30980  dya2iocnei  31542  dstfrvunirn  31734  pconnconn  32480  cvmcov2  32524  cvmlift2lem11  32562  cvmlift2lem12  32563  neibastop2lem  33710  onint1  33799  icoreunrn  34642  opnmbllem0  34930  heibor1  35090  unichnidl  35311  prtlem16  36007  prter2  36019  truniALT  40882  unipwrVD  41173  unipwr  41174  truniALTVD  41219  unisnALT  41267  restuni3  41391  disjinfi  41461  stoweidlem43  42335  stoweidlem55  42347  salexct  42624