Theorem elunii 4909

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 2823	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2822	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3586	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 670	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4907	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 233	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∪ cuni 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-uni 4905

This theorem is referenced by:  ssuni  4932  unipw  5446  opeluu  5466  unon  7806  limuni3  7828  uniinqs  8779  trcl  9710  rankwflemb  9775  ac5num  10018  dfac3  10103  isf34lem4  10359  axcclem  10439  ttukeylem7  10497  brdom7disj  10513  brdom6disj  10514  wrdexb  14462  dprdfeq0  19875  tgss2  22459  ppttop  22479  isclo  22560  neips  22586  2ndcomap  22931  2ndcsep  22932  locfincmp  22999  comppfsc  23005  txkgen  23125  txconn  23162  basqtop  23184  nrmr0reg  23222  alexsublem  23517  alexsubALTlem4  23523  alexsubALT  23524  ptcmplem4  23528  unirnblps  23894  unirnbl  23895  blbas  23905  met2ndci  24000  bndth  24443  dyadmbllem  25085  opnmbllem  25087  ssmxidllem  32538  dya2iocnei  33212  dstfrvunirn  33404  pconnconn  34153  cvmcov2  34197  cvmlift2lem11  34235  cvmlift2lem12  34236  neibastop2lem  35150  onint1  35239  icoreunrn  36145  opnmbllem0  36429  heibor1  36584  unichnidl  36805  prtlem16  37645  prter2  37657  naddsuc2  42014  truniALT  43173  unipwrVD  43464  unipwr  43465  truniALTVD  43510  unisnALT  43558  restuni3  43678  disjinfi  43762  stoweidlem43  44632  stoweidlem55  44644  salexct  44923