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 2826	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2825	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 633	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3553	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 672	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4868	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-uni 4866

This theorem is referenced by:  ssuni  4890  unipw  5405  opeluu  5426  unon  7783  limuni3  7804  naddsuc2  8639  uniinqs  8746  trcl  9649  rankwflemb  9717  ac5num  9958  dfac3  10043  isf34lem4  10299  axcclem  10379  ttukeylem7  10437  brdom7disj  10453  brdom6disj  10454  wrdexb  14460  dprdfeq0  19965  tgss2  22943  ppttop  22963  isclo  23043  neips  23069  2ndcomap  23414  2ndcsep  23415  locfincmp  23482  comppfsc  23488  txkgen  23608  txconn  23645  basqtop  23667  nrmr0reg  23705  alexsublem  24000  alexsubALTlem4  24006  alexsubALT  24007  ptcmplem4  24011  unirnblps  24375  unirnbl  24376  blbas  24386  met2ndci  24478  bndth  24925  dyadmbllem  25568  opnmbllem  25570  ssdifidllem  33549  ssmxidllem  33566  dya2iocnei  34460  dstfrvunirn  34653  pconnconn  35447  cvmcov2  35491  cvmlift2lem11  35529  cvmlift2lem12  35530  neibastop2lem  36576  onint1  36665  icoreunrn  37614  opnmbllem0  37907  heibor1  38061  unichnidl  38282  prtlem16  39245  prter2  39257  truniALT  44897  unipwrVD  45187  unipwr  45188  truniALTVD  45233  unisnALT  45281  permaxun  45367  restuni3  45477  disjinfi  45551  stoweidlem43  46401  stoweidlem55  46413  salexct  46692