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

Theorem spcegv 3442
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 2911 . 2 𝑥𝐴
2 nfv 1993 . 2 𝑥𝜓
3 spcgv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3spcegf 3437 1 (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1629  wex 1850  wcel 2143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-v 3350
This theorem is referenced by:  spcev  3448  elabd  3500  eqeu  3526  absneu  4396  issn  4493  elpreqprlem  4529  elunii  4576  axpweq  4969  brcogw  5428  opeldmd  5464  breldmg  5467  dmsnopg  5747  fvrnressn  6569  f1oexbi  7261  zfrep6  7279  unielxp  7351  wfrlem15  7580  ertr  7909  f1oen3g  8123  f1dom2g  8125  f1domg  8127  dom3d  8149  fodomr  8265  disjenex  8272  domssex2  8274  domssex  8275  ordiso  8575  fowdom  8630  brwdom2  8632  infeq5i  8695  oncard  8984  cardsn  8993  infxpenc2lem2  9041  dfac8b  9052  dfac8clem  9053  ac10ct  9055  ac5num  9057  acni2  9067  acnlem  9069  finnisoeu  9134  aceq3lem  9141  dfacacn  9163  infpss  9239  cflem  9268  cflecard  9275  cfslb  9288  cofsmo  9291  coftr  9295  alephsing  9298  fin4i  9320  axdc4lem  9477  ac6num  9501  axdclem2  9542  gchi  9646  grothpw  9848  hasheqf1oi  13347  fz1isolem  13450  wrd2f1tovbij  13916  relexpindlem  14014  climeu  14497  fsum  14662  ntrivcvgn0  14841  fprod  14882  isacs1i  16531  mreacs  16532  brcici  16673  initoeu2lem2  16878  gsumval2a  17493  gsumval3lem2  18520  eltg3  20993  elptr  21603  uptx  21655  alexsubALTlem1  22077  ptcmplem3  22084  prdsxmslem2  22560  nbusgrf1o1  26501  cusgrexg  26581  cusgrfilem3  26594  sizusglecusg  26600  wlknwwlksnbij2  27032  wlkwwlkbij2  27039  wlksnwwlknvbij  27057  clwwlkvbij  27293  clwwlkvbijOLDOLD  27294  clwwlkvbijOLD  27295  numclwwlk1lem2  27551  aciunf1lem  29803  locfinref  30249  fnimage  32374  fnessref  32690  refssfne  32691  filnetlem4  32714  bj-restb  33379  fin2so  33729  unirep  33839  indexa  33860  rp-isfinite5  38389  nssd  39810  choicefi  39911  axccdom  39935  stoweidlem5  40740  stoweidlem27  40762  stoweidlem28  40763  stoweidlem31  40766  stoweidlem43  40778  stoweidlem44  40779  stoweidlem51  40786  stoweidlem59  40794  nsssmfmbflem  41507  sprbisymrel  42274  uspgrbisymrelALT  42288  irinitoringc  42594
  Copyright terms: Public domain W3C validator