MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elunii Structured version   Visualization version   GIF version

Theorem elunii 4599
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.
StepHypRef Expression
1 eleq2 2833 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eleq1 2832 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐶𝐵𝐶))
31, 2anbi12d 624 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝑥𝐶) ↔ (𝐴𝐵𝐵𝐶)))
43spcegv 3446 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶)))
54anabsi7 661 . 2 ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶))
6 eluni 4597 . 2 (𝐴 𝐶 ↔ ∃𝑥(𝐴𝑥𝑥𝐶))
75, 6sylibr 225 1 ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wex 1874  wcel 2155   cuni 4594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-uni 4595
This theorem is referenced by:  ssuni  4618  unipw  5074  opeluu  5094  unon  7229  limuni3  7250  uniinqs  8030  trcl  8819  rankwflemb  8871  ac5num  9110  dfac3  9195  isf34lem4  9452  axcclem  9532  ttukeylem7  9590  brdom7disj  9606  brdom6disj  9607  wrdexb  13497  dprdfeq0  18688  tgss2  21071  ppttop  21091  isclo  21171  neips  21197  2ndcomap  21541  2ndcsep  21542  locfincmp  21609  comppfsc  21615  txkgen  21735  txconn  21772  basqtop  21794  nrmr0reg  21832  alexsublem  22127  alexsubALTlem4  22133  alexsubALT  22134  ptcmplem4  22138  unirnblps  22503  unirnbl  22504  blbas  22514  met2ndci  22606  bndth  23036  dyadmbllem  23657  opnmbllem  23659  dya2iocnei  30791  dstfrvunirn  30984  pconnconn  31661  cvmcov2  31705  cvmlift2lem11  31743  cvmlift2lem12  31744  neibastop2lem  32798  onint1  32887  icoreunrn  33640  cnfin0  33673  opnmbllem0  33869  heibor1  34031  unichnidl  34252  prtlem16  34825  prter2  34837  truniALT  39419  unipwrVD  39720  unipwr  39721  truniALTVD  39766  unisnALT  39814  restuni3  39951  disjinfi  40027  stoweidlem43  40897  stoweidlem55  40909  salexct  41189
  Copyright terms: Public domain W3C validator