Theorem elunii 4824

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 2826	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2825	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 634	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3512	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 671	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4822	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 237	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2110  ∪ cuni 4819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-uni 4820

This theorem is referenced by:  ssuni  4846  unipw  5335  opeluu  5354  unon  7610  limuni3  7631  uniinqs  8479  trcl  9344  rankwflemb  9409  ac5num  9650  dfac3  9735  isf34lem4  9991  axcclem  10071  ttukeylem7  10129  brdom7disj  10145  brdom6disj  10146  wrdexb  14080  dprdfeq0  19409  tgss2  21884  ppttop  21904  isclo  21984  neips  22010  2ndcomap  22355  2ndcsep  22356  locfincmp  22423  comppfsc  22429  txkgen  22549  txconn  22586  basqtop  22608  nrmr0reg  22646  alexsublem  22941  alexsubALTlem4  22947  alexsubALT  22948  ptcmplem4  22952  unirnblps  23317  unirnbl  23318  blbas  23328  met2ndci  23420  bndth  23855  dyadmbllem  24496  opnmbllem  24498  ssmxidllem  31355  dya2iocnei  31961  dstfrvunirn  32153  pconnconn  32906  cvmcov2  32950  cvmlift2lem11  32988  cvmlift2lem12  32989  neibastop2lem  34286  onint1  34375  icoreunrn  35267  opnmbllem0  35550  heibor1  35705  unichnidl  35926  prtlem16  36620  prter2  36632  truniALT  41834  unipwrVD  42125  unipwr  42126  truniALTVD  42171  unisnALT  42219  restuni3  42340  disjinfi  42404  stoweidlem43  43259  stoweidlem55  43271  salexct  43548