Theorem elunii 4879

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 2854	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2853	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3558	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 684	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4877	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 237	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∪ cuni 4874

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-uni 4875

This theorem is used by:  ssuni  4900  unipw  5433  opeluu  5454  unon  7833  limuni3  7854  naddsuc2  8694  uniinqs  8801  trcl  9704  rankwflemb  9772  ac5num  10036  dfac3  10121  isf34lem4  10376  axcclem  10456  ttukeylem7  10514  brdom7disj  10530  brdom6disj  10531  wrdexb  14580  dprdfeq0  20138  unichnlidl  21412  ssdifidllem  21534  tgss2  23194  ppttop  23214  isclo  23294  neips  23320  2ndcomap  23666  2ndcsep  23667  locfincmp  23734  comppfsc  23740  txkgen  23860  txconn  23897  basqtop  23919  nrmr0reg  23957  alexsublem  24252  alexsubALTlem4  24258  alexsubALT  24259  ptcmplem4  24263  unirnblps  24627  unirnbl  24628  blbas  24638  met2ndci  24730  bndth  25168  dyadmbllem  25809  opnmbllem  25811  ssmxidllem  33820  dya2iocnei  34737  dstfrvunirn  34930  pconnconn  35760  cvmcov2  35804  cvmlift2lem11  35842  cvmlift2lem12  35843  neibastop2lem  36928  onint1  37017  ttcid  37060  ttctr  37061  dfttc2g  37074  icoreunrn  38062  opnmbllem0  38364  heibor1  38519  unichnidl  38740  prtlem16  39701  prter2  39713  truniALT  45308  unipwrVD  45598  unipwr  45599  truniALTVD  45644  unisnALT  45692  permaxun  45778  restuni3  45894  disjinfi  45968  stoweidlem43  46815  stoweidlem55  46827  salexct  47106