Theorem elunii 4912

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-uni 4908

This theorem is referenced by:  ssuni  4932  unipw  5455  opeluu  5475  unon  7851  limuni3  7873  naddsuc2  8739  uniinqs  8837  trcl  9768  rankwflemb  9833  ac5num  10076  dfac3  10161  isf34lem4  10417  axcclem  10497  ttukeylem7  10555  brdom7disj  10571  brdom6disj  10572  wrdexb  14563  dprdfeq0  20042  tgss2  22994  ppttop  23014  isclo  23095  neips  23121  2ndcomap  23466  2ndcsep  23467  locfincmp  23534  comppfsc  23540  txkgen  23660  txconn  23697  basqtop  23719  nrmr0reg  23757  alexsublem  24052  alexsubALTlem4  24058  alexsubALT  24059  ptcmplem4  24063  unirnblps  24429  unirnbl  24430  blbas  24440  met2ndci  24535  bndth  24990  dyadmbllem  25634  opnmbllem  25636  ssdifidllem  33484  ssmxidllem  33501  dya2iocnei  34284  dstfrvunirn  34477  pconnconn  35236  cvmcov2  35280  cvmlift2lem11  35318  cvmlift2lem12  35319  neibastop2lem  36361  onint1  36450  icoreunrn  37360  opnmbllem0  37663  heibor1  37817  unichnidl  38038  prtlem16  38870  prter2  38882  truniALT  44561  unipwrVD  44852  unipwr  44853  truniALTVD  44898  unisnALT  44946  restuni3  45123  disjinfi  45197  stoweidlem43  46058  stoweidlem55  46070  salexct  46349