Theorem elunii 4861

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∪ cuni 4856

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-uni 4857

This theorem is referenced by:  ssuni  4881  unipw  5389  opeluu  5408  unon  7761  limuni3  7782  naddsuc2  8616  uniinqs  8721  trcl  9618  rankwflemb  9686  ac5num  9927  dfac3  10012  isf34lem4  10268  axcclem  10348  ttukeylem7  10406  brdom7disj  10422  brdom6disj  10423  wrdexb  14432  dprdfeq0  19936  tgss2  22902  ppttop  22922  isclo  23002  neips  23028  2ndcomap  23373  2ndcsep  23374  locfincmp  23441  comppfsc  23447  txkgen  23567  txconn  23604  basqtop  23626  nrmr0reg  23664  alexsublem  23959  alexsubALTlem4  23965  alexsubALT  23966  ptcmplem4  23970  unirnblps  24334  unirnbl  24335  blbas  24345  met2ndci  24437  bndth  24884  dyadmbllem  25527  opnmbllem  25529  ssdifidllem  33421  ssmxidllem  33438  dya2iocnei  34295  dstfrvunirn  34488  pconnconn  35275  cvmcov2  35319  cvmlift2lem11  35357  cvmlift2lem12  35358  neibastop2lem  36402  onint1  36491  icoreunrn  37401  opnmbllem0  37704  heibor1  37858  unichnidl  38079  prtlem16  38916  prter2  38928  truniALT  44582  unipwrVD  44872  unipwr  44873  truniALTVD  44918  unisnALT  44966  permaxun  45052  restuni3  45163  disjinfi  45237  stoweidlem43  46089  stoweidlem55  46101  salexct  46380