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

Theorem elunii 4909
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 2823 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eleq1 2822 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐶𝐵𝐶))
31, 2anbi12d 632 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝑥𝐶) ↔ (𝐴𝐵𝐵𝐶)))
43spcegv 3586 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶)))
54anabsi7 670 . 2 ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶))
6 eluni 4907 . 2 (𝐴 𝐶 ↔ ∃𝑥(𝐴𝑥𝑥𝐶))
75, 6sylibr 233 1 ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wex 1782  wcel 2107   cuni 4904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-uni 4905
This theorem is referenced by:  ssuni  4932  unipw  5446  opeluu  5466  unon  7806  limuni3  7828  uniinqs  8779  trcl  9710  rankwflemb  9775  ac5num  10018  dfac3  10103  isf34lem4  10359  axcclem  10439  ttukeylem7  10497  brdom7disj  10513  brdom6disj  10514  wrdexb  14462  dprdfeq0  19875  tgss2  22459  ppttop  22479  isclo  22560  neips  22586  2ndcomap  22931  2ndcsep  22932  locfincmp  22999  comppfsc  23005  txkgen  23125  txconn  23162  basqtop  23184  nrmr0reg  23222  alexsublem  23517  alexsubALTlem4  23523  alexsubALT  23524  ptcmplem4  23528  unirnblps  23894  unirnbl  23895  blbas  23905  met2ndci  24000  bndth  24443  dyadmbllem  25085  opnmbllem  25087  ssmxidllem  32538  dya2iocnei  33212  dstfrvunirn  33404  pconnconn  34153  cvmcov2  34197  cvmlift2lem11  34235  cvmlift2lem12  34236  neibastop2lem  35150  onint1  35239  icoreunrn  36145  opnmbllem0  36429  heibor1  36584  unichnidl  36805  prtlem16  37645  prter2  37657  naddsuc2  42014  truniALT  43173  unipwrVD  43464  unipwr  43465  truniALTVD  43510  unisnALT  43558  restuni3  43678  disjinfi  43762  stoweidlem43  44632  stoweidlem55  44644  salexct  44923
  Copyright terms: Public domain W3C validator