Theorem elunii 4863

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-uni 4859

This theorem is referenced by:  ssuni  4883  unipw  5393  opeluu  5413  unon  7764  limuni3  7785  naddsuc2  8619  uniinqs  8724  trcl  9624  rankwflemb  9689  ac5num  9930  dfac3  10015  isf34lem4  10271  axcclem  10351  ttukeylem7  10409  brdom7disj  10425  brdom6disj  10426  wrdexb  14432  dprdfeq0  19903  tgss2  22872  ppttop  22892  isclo  22972  neips  22998  2ndcomap  23343  2ndcsep  23344  locfincmp  23411  comppfsc  23417  txkgen  23537  txconn  23574  basqtop  23596  nrmr0reg  23634  alexsublem  23929  alexsubALTlem4  23935  alexsubALT  23936  ptcmplem4  23940  unirnblps  24305  unirnbl  24306  blbas  24316  met2ndci  24408  bndth  24855  dyadmbllem  25498  opnmbllem  25500  ssdifidllem  33393  ssmxidllem  33410  dya2iocnei  34250  dstfrvunirn  34443  pconnconn  35204  cvmcov2  35248  cvmlift2lem11  35286  cvmlift2lem12  35287  neibastop2lem  36334  onint1  36423  icoreunrn  37333  opnmbllem0  37636  heibor1  37790  unichnidl  38011  prtlem16  38848  prter2  38860  truniALT  44515  unipwrVD  44805  unipwr  44806  truniALTVD  44851  unisnALT  44899  permaxun  44985  restuni3  45096  disjinfi  45170  stoweidlem43  46024  stoweidlem55  46036  salexct  46315