Theorem elunii 4877

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-uni 4873

This theorem is used by:  ssuni  4898  unipw  5425  opeluu  5446  unon  7876  limuni3  7897  naddsuc2  8749  uniinqs  8856  trcl  9766  rankwflemb  9837  rankwflembOLD  9838  ac5num  10154  dfac3  10239  isf34lem4  10494  axcclem  10574  ttukeylem7  10632  brdom7disj  10649  brdom6disj  10650  wrdexb  14711  dprdfeq0  20289  unichnlidl  21567  ssdifidllem  21691  tgss2  23360  ppttop  23380  isclo  23460  neips  23486  2ndcomap  23832  2ndcsep  23833  locfincmp  23900  comppfsc  23906  txkgen  24026  txconn  24063  basqtop  24085  nrmr0reg  24123  alexsublem  24418  alexsubALTlem4  24424  alexsubALT  24425  ptcmplem4  24429  unirnblps  24793  unirnbl  24794  blbas  24804  met2ndci  24896  bndth  25334  dyadmbllem  25975  opnmbllem  25977  ssmxidllem  34102  dya2iocnei  35025  dstfrvunirn  35218  pconnconn  36204  cvmcov2  36248  cvmlift2lem11  36286  cvmlift2lem12  36287  neibastop2lem  37363  onint1  37452  ttcid  37495  ttctr  37496  dfttc2g  37509  icoreunrn  38550  opnmbllem0  38842  heibor1  39010  unichnidl  39231  prtlem16  40192  prter2  40204  truniALT  45784  unipwrVD  46074  unipwr  46075  truniALTVD  46120  unisnALT  46168  permaxun  46265  restuni3  46406  disjinfi  46480  stoweidlem43  47326  stoweidlem55  47338  salexct  47617