Theorem elunii 4841

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 2827	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2826	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 630	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3526	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 667	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4839	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 233	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-uni 4837

This theorem is referenced by:  ssuni  4863  unipw  5360  opeluu  5379  unon  7653  limuni3  7674  uniinqs  8544  trcl  9417  rankwflemb  9482  ac5num  9723  dfac3  9808  isf34lem4  10064  axcclem  10144  ttukeylem7  10202  brdom7disj  10218  brdom6disj  10219  wrdexb  14156  dprdfeq0  19540  tgss2  22045  ppttop  22065  isclo  22146  neips  22172  2ndcomap  22517  2ndcsep  22518  locfincmp  22585  comppfsc  22591  txkgen  22711  txconn  22748  basqtop  22770  nrmr0reg  22808  alexsublem  23103  alexsubALTlem4  23109  alexsubALT  23110  ptcmplem4  23114  unirnblps  23480  unirnbl  23481  blbas  23491  met2ndci  23584  bndth  24027  dyadmbllem  24668  opnmbllem  24670  ssmxidllem  31543  dya2iocnei  32149  dstfrvunirn  32341  pconnconn  33093  cvmcov2  33137  cvmlift2lem11  33175  cvmlift2lem12  33176  neibastop2lem  34476  onint1  34565  icoreunrn  35457  opnmbllem0  35740  heibor1  35895  unichnidl  36116  prtlem16  36810  prter2  36822  truniALT  42050  unipwrVD  42341  unipwr  42342  truniALTVD  42387  unisnALT  42435  restuni3  42556  disjinfi  42620  stoweidlem43  43474  stoweidlem55  43486  salexct  43763