Theorem elunii 4917

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ∃wex 1776   ∈ wcel 2106  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-uni 4913

This theorem is referenced by:  ssuni  4937  unipw  5461  opeluu  5481  unon  7851  limuni3  7873  naddsuc2  8738  uniinqs  8836  trcl  9766  rankwflemb  9831  ac5num  10074  dfac3  10159  isf34lem4  10415  axcclem  10495  ttukeylem7  10553  brdom7disj  10569  brdom6disj  10570  wrdexb  14560  dprdfeq0  20057  tgss2  23010  ppttop  23030  isclo  23111  neips  23137  2ndcomap  23482  2ndcsep  23483  locfincmp  23550  comppfsc  23556  txkgen  23676  txconn  23713  basqtop  23735  nrmr0reg  23773  alexsublem  24068  alexsubALTlem4  24074  alexsubALT  24075  ptcmplem4  24079  unirnblps  24445  unirnbl  24446  blbas  24456  met2ndci  24551  bndth  25004  dyadmbllem  25648  opnmbllem  25650  ssdifidllem  33464  ssmxidllem  33481  dya2iocnei  34264  dstfrvunirn  34456  pconnconn  35216  cvmcov2  35260  cvmlift2lem11  35298  cvmlift2lem12  35299  neibastop2lem  36343  onint1  36432  icoreunrn  37342  opnmbllem0  37643  heibor1  37797  unichnidl  38018  prtlem16  38851  prter2  38863  truniALT  44539  unipwrVD  44830  unipwr  44831  truniALTVD  44876  unisnALT  44924  restuni3  45058  disjinfi  45135  stoweidlem43  45999  stoweidlem55  46011  salexct  46290