Theorem elunii 4870

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 2851	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2850	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 641	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3556	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 681	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4868	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 236	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560  ∃wex 1799   ∈ wcel 2142  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-uni 4866

This theorem is referenced by:  ssuni  4891  unipw  5417  opeluu  5438  unon  7811  limuni3  7832  naddsuc2  8672  uniinqs  8779  trcl  9683  rankwflemb  9751  ac5num  9992  dfac3  10077  isf34lem4  10334  axcclem  10414  ttukeylem7  10472  brdom7disj  10488  brdom6disj  10489  wrdexb  14538  dprdfeq0  20064  tgss2  23044  ppttop  23064  isclo  23144  neips  23170  2ndcomap  23515  2ndcsep  23516  locfincmp  23583  comppfsc  23589  txkgen  23709  txconn  23746  basqtop  23768  nrmr0reg  23806  alexsublem  24101  alexsubALTlem4  24107  alexsubALT  24108  ptcmplem4  24112  unirnblps  24476  unirnbl  24477  blbas  24487  met2ndci  24579  bndth  25017  dyadmbllem  25658  opnmbllem  25660  ssdifidllem  33640  ssmxidllem  33658  dya2iocnei  34576  dstfrvunirn  34769  pconnconn  35578  cvmcov2  35622  cvmlift2lem11  35660  cvmlift2lem12  35661  neibastop2lem  36717  onint1  36806  ttcid  36849  ttctr  36850  dfttc2g  36863  icoreunrn  37850  opnmbllem0  38152  heibor1  38306  unichnidl  38527  prtlem16  39490  prter2  39502  truniALT  45114  unipwrVD  45404  unipwr  45405  truniALTVD  45450  unisnALT  45498  permaxun  45584  restuni3  45693  disjinfi  45767  stoweidlem43  46614  stoweidlem55  46626  salexct  46905