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

Theorem spcegv 3289
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 2762 . 2 𝑥𝐴
2 nfv 1841 . 2 𝑥𝜓
3 spcgv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3spcegf 3284 1 (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wex 1702  wcel 1988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197
This theorem is referenced by:  spcev  3295  elabd  3346  eqeu  3371  absneu  4254  issn  4354  elpreqprlem  4386  elunii  4432  axpweq  4833  brcogw  5279  opeldmd  5316  breldmg  5319  dmsnopg  5594  fvrnressn  6413  f1oexbi  7101  zfrep6  7119  unielxp  7189  wfrlem15  7414  ertr  7742  f1oen3g  7956  f1dom2g  7958  f1domg  7960  dom3d  7982  fodomr  8096  disjenex  8103  domssex2  8105  domssex  8106  ordiso  8406  fowdom  8461  brwdom2  8463  infeq5i  8518  oncard  8771  cardsn  8780  infxpenc2lem2  8828  dfac8b  8839  dfac8clem  8840  ac10ct  8842  ac5num  8844  acni2  8854  acnlem  8856  finnisoeu  8921  aceq3lem  8928  dfacacn  8948  infpss  9024  cflem  9053  cflecard  9060  cfslb  9073  cofsmo  9076  coftr  9080  alephsing  9083  fin4i  9105  axdc4lem  9262  ac6num  9286  axdclem2  9327  gchi  9431  grothpw  9633  hasheqf1oi  13123  hasheqf1oiOLD  13124  fz1isolem  13228  wrd2f1tovbij  13684  relexpindlem  13784  climeu  14267  fsum  14432  ntrivcvgn0  14611  fprod  14652  isacs1i  16299  mreacs  16300  brcici  16441  initoeu2lem2  16646  gsumval2a  17260  gsumval3lem2  18288  eltg3  20747  elptr  21357  uptx  21409  alexsubALTlem1  21832  ptcmplem3  21839  prdsxmslem2  22315  nbusgrf1o1  26253  cusgrexg  26321  cusgrfilem3  26334  sizusglecusg  26340  wlknwwlksnbij2  26759  wlkwwlkbij2  26766  wlksnwwlknvbij  26784  clwwlksbij  26900  clwwlksvbij  26902  numclwlk1lem2  27201  rmoeqALT  29299  aciunf1lem  29435  locfinref  29882  fnimage  32011  fnessref  32327  refssfne  32328  filnetlem4  32351  bj-restb  33022  fin2so  33367  unirep  33478  indexa  33499  rp-isfinite5  37682  nssd  39108  choicefi  39208  axccdom  39232  stoweidlem5  39985  stoweidlem27  40007  stoweidlem28  40008  stoweidlem31  40011  stoweidlem43  40023  stoweidlem44  40024  stoweidlem51  40031  stoweidlem59  40039  nsssmfmbflem  40749  sprbisymrel  41514  uspgrbisymrelALT  41528  irinitoringc  41834
  Copyright terms: Public domain W3C validator