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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-uni 4859

This theorem is referenced by:  ssuni  4883  unipw  5393  opeluu  5413  unon  7767  limuni3  7788  naddsuc2  8622  uniinqs  8727  trcl  9624  rankwflemb  9692  ac5num  9933  dfac3  10018  isf34lem4  10274  axcclem  10354  ttukeylem7  10412  brdom7disj  10428  brdom6disj  10429  wrdexb  14438  dprdfeq0  19942  tgss2  22908  ppttop  22928  isclo  23008  neips  23034  2ndcomap  23379  2ndcsep  23380  locfincmp  23447  comppfsc  23453  txkgen  23573  txconn  23610  basqtop  23632  nrmr0reg  23670  alexsublem  23965  alexsubALTlem4  23971  alexsubALT  23972  ptcmplem4  23976  unirnblps  24340  unirnbl  24341  blbas  24351  met2ndci  24443  bndth  24890  dyadmbllem  25533  opnmbllem  25535  ssdifidllem  33428  ssmxidllem  33445  dya2iocnei  34302  dstfrvunirn  34495  pconnconn  35282  cvmcov2  35326  cvmlift2lem11  35364  cvmlift2lem12  35365  neibastop2lem  36411  onint1  36500  icoreunrn  37410  opnmbllem0  37702  heibor1  37856  unichnidl  38077  prtlem16  38974  prter2  38986  truniALT  44639  unipwrVD  44929  unipwr  44930  truniALTVD  44975  unisnALT  45023  permaxun  45109  restuni3  45220  disjinfi  45294  stoweidlem43  46146  stoweidlem55  46158  salexct  46437