Theorem elunii 4936

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 2833	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2832	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 631	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3610	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 670	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4934	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-uni 4932

This theorem is referenced by:  ssuni  4956  unipw  5470  opeluu  5490  unon  7867  limuni3  7889  naddsuc2  8757  uniinqs  8855  trcl  9797  rankwflemb  9862  ac5num  10105  dfac3  10190  isf34lem4  10446  axcclem  10526  ttukeylem7  10584  brdom7disj  10600  brdom6disj  10601  wrdexb  14573  dprdfeq0  20066  tgss2  23015  ppttop  23035  isclo  23116  neips  23142  2ndcomap  23487  2ndcsep  23488  locfincmp  23555  comppfsc  23561  txkgen  23681  txconn  23718  basqtop  23740  nrmr0reg  23778  alexsublem  24073  alexsubALTlem4  24079  alexsubALT  24080  ptcmplem4  24084  unirnblps  24450  unirnbl  24451  blbas  24461  met2ndci  24556  bndth  25009  dyadmbllem  25653  opnmbllem  25655  ssdifidllem  33449  ssmxidllem  33466  dya2iocnei  34247  dstfrvunirn  34439  pconnconn  35199  cvmcov2  35243  cvmlift2lem11  35281  cvmlift2lem12  35282  neibastop2lem  36326  onint1  36415  icoreunrn  37325  opnmbllem0  37616  heibor1  37770  unichnidl  37991  prtlem16  38825  prter2  38837  truniALT  44512  unipwrVD  44803  unipwr  44804  truniALTVD  44849  unisnALT  44897  restuni3  45020  disjinfi  45099  stoweidlem43  45964  stoweidlem55  45976  salexct  46255