Theorem elunii 4868

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-uni 4864

This theorem is referenced by:  ssuni  4888  unipw  5398  opeluu  5418  unon  7773  limuni3  7794  naddsuc2  8629  uniinqs  8734  trcl  9637  rankwflemb  9705  ac5num  9946  dfac3  10031  isf34lem4  10287  axcclem  10367  ttukeylem7  10425  brdom7disj  10441  brdom6disj  10442  wrdexb  14448  dprdfeq0  19953  tgss2  22931  ppttop  22951  isclo  23031  neips  23057  2ndcomap  23402  2ndcsep  23403  locfincmp  23470  comppfsc  23476  txkgen  23596  txconn  23633  basqtop  23655  nrmr0reg  23693  alexsublem  23988  alexsubALTlem4  23994  alexsubALT  23995  ptcmplem4  23999  unirnblps  24363  unirnbl  24364  blbas  24374  met2ndci  24466  bndth  24913  dyadmbllem  25556  opnmbllem  25558  ssdifidllem  33537  ssmxidllem  33554  dya2iocnei  34439  dstfrvunirn  34632  pconnconn  35425  cvmcov2  35469  cvmlift2lem11  35507  cvmlift2lem12  35508  neibastop2lem  36554  onint1  36643  icoreunrn  37564  opnmbllem0  37857  heibor1  38011  unichnidl  38232  prtlem16  39129  prter2  39141  truniALT  44782  unipwrVD  45072  unipwr  45073  truniALTVD  45118  unisnALT  45166  permaxun  45252  restuni3  45362  disjinfi  45436  stoweidlem43  46287  stoweidlem55  46299  salexct  46578