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

Theorem spcegv 3267
 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 2751 . 2 𝑥𝐴
2 nfv 1830 . 2 𝑥𝜓
3 spcgv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3spcegf 3262 1 (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∃wex 1695   ∈ wcel 1977 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175 This theorem is referenced by:  spcev  3273  elabd  3321  eqeu  3344  absneu  4207  issn  4303  elpreqprlem  4333  elunii  4377  axpweq  4768  brcogw  5212  opeldmd  5249  breldmg  5252  dmsnopg  5524  fvrnressn  6333  f1oexbi  7009  zfrep6  7027  unielxp  7095  wfrlem15  7316  ertr  7644  f1oen3g  7857  f1dom2g  7859  f1domg  7861  dom3d  7883  fodomr  7996  disjenex  8003  domssex2  8005  domssex  8006  ordiso  8304  fowdom  8359  brwdom2  8361  infeq5i  8416  oncard  8669  cardsn  8678  infxpenc2lem2  8726  dfac8b  8737  dfac8clem  8738  ac10ct  8740  ac5num  8742  acni2  8752  acnlem  8754  finnisoeu  8819  aceq3lem  8826  dfacacn  8846  infpss  8922  cflem  8951  cflecard  8958  cfslb  8971  cofsmo  8974  coftr  8978  alephsing  8981  fin4i  9003  axdc4lem  9160  ac6num  9184  axdclem2  9225  gchi  9325  grothpw  9527  hasheqf1oi  13002  hasheqf1oiOLD  13003  fz1isolem  13102  wrd2f1tovbij  13551  relexpindlem  13651  climeu  14134  fsum  14298  ntrivcvgn0  14469  fprod  14510  isacs1i  16141  mreacs  16142  brcici  16283  initoeu2lem2  16488  gsumval2a  17102  gsumval3lem2  18130  eltg3  20577  elptr  21186  uptx  21238  alexsubALTlem1  21661  ptcmplem3  21668  prdsxmslem2  22144  nbgraf1o0  25975  cusgraexg  25998  cusgrafilem3  26009  wlknwwlknbij2  26242  wlkiswwlkbij2  26249  wwlkextbij  26261  wlknwwlknvbij  26268  clwwlkbij  26327  clwwlkvbij  26329  frgrancvvdeqlem9  26568  numclwlk1lem2  26624  rmoeqALT  28711  aciunf1lem  28844  locfinref  29236  fnimage  31206  fnessref  31522  refssfne  31523  filnetlem4  31546  bj-restb  32228  fin2so  32566  unirep  32677  indexa  32698  rp-isfinite5  36882  nssd  38317  choicefi  38387  axccdom  38411  stoweidlem5  38898  stoweidlem27  38920  stoweidlem28  38921  stoweidlem31  38924  stoweidlem43  38936  stoweidlem44  38937  stoweidlem51  38944  stoweidlem59  38952  nsssmfmbflem  39664  nbusgrf1o1  40598  cusgrexg  40663  cusgrfilem3  40673  sizusglecusg  40679  wlknwwlksnbij2  41089  wlkwwlkbij2  41096  wlksnwwlknvbij  41114  clwwlksbij  41227  clwwlksvbij  41229  av-numclwlk1lem2  41527  irinitoringc  41861
 Copyright terms: Public domain W3C validator