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

Theorem spcegv 3266
Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
spcgv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
spcegv (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem spcegv
StepHypRef Expression
1 nfcv 2750 . 2 𝑥𝐴
2 nfv 1829 . 2 𝑥𝜓
3 spcgv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3spcegf 3261 1 (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wex 1694  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174
This theorem is referenced by:  spcev  3272  elabd  3320  eqeu  3343  absneu  4206  elpreqprlem  4328  elunii  4371  axpweq  4763  brcogw  5200  opeldmd  5236  breldmg  5239  dmsnopg  5510  fvrnressn  6311  f1oexbi  6986  zfrep6  7004  unielxp  7072  wfrlem15  7293  ertr  7621  f1oen3g  7834  f1dom2g  7836  f1domg  7838  dom3d  7860  fodomr  7973  disjenex  7980  domssex2  7982  domssex  7983  ordiso  8281  fowdom  8336  brwdom2  8338  infeq5i  8393  oncard  8646  cardsn  8655  infxpenc2lem2  8703  dfac8b  8714  dfac8clem  8715  ac10ct  8717  ac5num  8719  acni2  8729  acnlem  8731  finnisoeu  8796  aceq3lem  8803  dfacacn  8823  infpss  8899  cflem  8928  cflecard  8935  cfslb  8948  cofsmo  8951  coftr  8955  alephsing  8958  fin4i  8980  axdc4lem  9137  ac6num  9161  axdclem2  9202  gchi  9302  grothpw  9504  hasheqf1oi  12954  hasheqf1oiOLD  12955  fz1isolem  13054  wrd2f1tovbij  13497  relexpindlem  13597  climeu  14080  fsum  14244  ntrivcvgn0  14415  fprod  14456  isacs1i  16087  mreacs  16088  brcici  16229  initoeu2lem2  16434  gsumval2a  17048  gsumval3lem2  18076  eltg3  20519  elptr  21128  uptx  21180  alexsubALTlem1  21603  ptcmplem3  21610  prdsxmslem2  22085  nbgraf1o0  25741  cusgraexg  25764  cusgrafilem3  25775  wlknwwlknbij2  26008  wlkiswwlkbij2  26015  wwlkextbij  26027  wlknwwlknvbij  26034  clwwlkbij  26093  clwwlkvbij  26095  frgrancvvdeqlem9  26334  numclwlk1lem2  26390  rmoeqALT  28517  aciunf1lem  28650  locfinref  29042  fnimage  31012  fnessref  31328  refssfne  31329  filnetlem4  31352  bj-restb  32024  fin2so  32362  unirep  32473  indexa  32494  rp-isfinite5  36678  nssd  38113  choicefi  38183  axccdom  38207  stoweidlem5  38695  stoweidlem27  38717  stoweidlem28  38718  stoweidlem31  38721  stoweidlem43  38733  stoweidlem44  38734  stoweidlem51  38741  stoweidlem59  38749  nsssmfmbflem  39461  issn  40115  nbusgrf1o1  40593  cusgrexg  40658  cusgrfilem3  40668  sizusglecusg  40674  wlknwwlksnbij2  41084  wlkwwlkbij2  41091  wlksnwwlknvbij  41109  clwwlksbij  41222  clwwlksvbij  41224  av-numclwlk1lem2  41522  irinitoringc  41856
  Copyright terms: Public domain W3C validator