Theorem elunii 4866

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

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

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-uni 4862

This theorem is referenced by:  ssuni  4886  unipw  5396  opeluu  5416  unon  7771  limuni3  7792  naddsuc2  8627  uniinqs  8732  trcl  9635  rankwflemb  9703  ac5num  9944  dfac3  10029  isf34lem4  10285  axcclem  10365  ttukeylem7  10423  brdom7disj  10439  brdom6disj  10440  wrdexb  14446  dprdfeq0  19951  tgss2  22929  ppttop  22949  isclo  23029  neips  23055  2ndcomap  23400  2ndcsep  23401  locfincmp  23468  comppfsc  23474  txkgen  23594  txconn  23631  basqtop  23653  nrmr0reg  23691  alexsublem  23986  alexsubALTlem4  23992  alexsubALT  23993  ptcmplem4  23997  unirnblps  24361  unirnbl  24362  blbas  24372  met2ndci  24464  bndth  24911  dyadmbllem  25554  opnmbllem  25556  ssdifidllem  33486  ssmxidllem  33503  dya2iocnei  34388  dstfrvunirn  34581  pconnconn  35374  cvmcov2  35418  cvmlift2lem11  35456  cvmlift2lem12  35457  neibastop2lem  36503  onint1  36592  icoreunrn  37503  opnmbllem0  37796  heibor1  37950  unichnidl  38171  prtlem16  39068  prter2  39080  truniALT  44724  unipwrVD  45014  unipwr  45015  truniALTVD  45060  unisnALT  45108  permaxun  45194  restuni3  45304  disjinfi  45378  stoweidlem43  46229  stoweidlem55  46241  salexct  46520