Theorem elunii 4872

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 3560	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 671	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4870	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

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

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 3446  df-uni 4868

This theorem is referenced by:  ssuni  4892  unipw  5405  opeluu  5425  unon  7786  limuni3  7808  naddsuc2  8642  uniinqs  8747  trcl  9657  rankwflemb  9722  ac5num  9965  dfac3  10050  isf34lem4  10306  axcclem  10386  ttukeylem7  10444  brdom7disj  10460  brdom6disj  10461  wrdexb  14466  dprdfeq0  19930  tgss2  22850  ppttop  22870  isclo  22950  neips  22976  2ndcomap  23321  2ndcsep  23322  locfincmp  23389  comppfsc  23395  txkgen  23515  txconn  23552  basqtop  23574  nrmr0reg  23612  alexsublem  23907  alexsubALTlem4  23913  alexsubALT  23914  ptcmplem4  23918  unirnblps  24283  unirnbl  24284  blbas  24294  met2ndci  24386  bndth  24833  dyadmbllem  25476  opnmbllem  25478  ssdifidllem  33400  ssmxidllem  33417  dya2iocnei  34246  dstfrvunirn  34439  pconnconn  35191  cvmcov2  35235  cvmlift2lem11  35273  cvmlift2lem12  35274  neibastop2lem  36321  onint1  36410  icoreunrn  37320  opnmbllem0  37623  heibor1  37777  unichnidl  37998  prtlem16  38835  prter2  38847  truniALT  44504  unipwrVD  44794  unipwr  44795  truniALTVD  44840  unisnALT  44888  permaxun  44974  restuni3  45085  disjinfi  45159  stoweidlem43  46014  stoweidlem55  46026  salexct  46305