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

Theorem spcegv 3325
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 2793 . 2 𝑥𝐴
2 nfv 1883 . 2 𝑥𝜓
3 spcgv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3spcegf 3320 1 (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wex 1744  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233
This theorem is referenced by:  spcev  3331  elabd  3384  eqeu  3410  absneu  4295  issn  4395  elpreqprlem  4426  elunii  4473  axpweq  4872  brcogw  5323  opeldmd  5359  breldmg  5362  dmsnopg  5642  fvrnressn  6468  f1oexbi  7158  zfrep6  7176  unielxp  7248  wfrlem15  7474  ertr  7802  f1oen3g  8013  f1dom2g  8015  f1domg  8017  dom3d  8039  fodomr  8152  disjenex  8159  domssex2  8161  domssex  8162  ordiso  8462  fowdom  8517  brwdom2  8519  infeq5i  8571  oncard  8824  cardsn  8833  infxpenc2lem2  8881  dfac8b  8892  dfac8clem  8893  ac10ct  8895  ac5num  8897  acni2  8907  acnlem  8909  finnisoeu  8974  aceq3lem  8981  dfacacn  9001  infpss  9077  cflem  9106  cflecard  9113  cfslb  9126  cofsmo  9129  coftr  9133  alephsing  9136  fin4i  9158  axdc4lem  9315  ac6num  9339  axdclem2  9380  gchi  9484  grothpw  9686  hasheqf1oi  13180  fz1isolem  13283  wrd2f1tovbij  13749  relexpindlem  13847  climeu  14330  fsum  14495  ntrivcvgn0  14674  fprod  14715  isacs1i  16365  mreacs  16366  brcici  16507  initoeu2lem2  16712  gsumval2a  17326  gsumval3lem2  18353  eltg3  20814  elptr  21424  uptx  21476  alexsubALTlem1  21898  ptcmplem3  21905  prdsxmslem2  22381  nbusgrf1o1  26316  cusgrexg  26396  cusgrfilem3  26409  sizusglecusg  26415  wlknwwlksnbij2  26846  wlkwwlkbij2  26853  wlksnwwlknvbij  26871  clwwlkbij  27015  clwwlkvbij  27088  clwwlkvbijOLD  27089  numclwlk1lem2  27350  aciunf1lem  29590  locfinref  30036  fnimage  32161  fnessref  32477  refssfne  32478  filnetlem4  32501  bj-restb  33172  fin2so  33526  unirep  33637  indexa  33658  rp-isfinite5  38180  nssd  39602  choicefi  39706  axccdom  39730  stoweidlem5  40540  stoweidlem27  40562  stoweidlem28  40563  stoweidlem31  40566  stoweidlem43  40578  stoweidlem44  40579  stoweidlem51  40586  stoweidlem59  40594  nsssmfmbflem  41307  sprbisymrel  42074  uspgrbisymrelALT  42088  irinitoringc  42394
  Copyright terms: Public domain W3C validator