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

Theorem spcegv 3581
Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2129, ax-11 2146. (Revised by Wolf Lammen, 25-Aug-2023.)
Hypothesis
Ref Expression
spcgv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
spcegv (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem spcegv
StepHypRef Expression
1 elisset 2807 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 spcgv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
32biimprcd 249 . . 3 (𝜓 → (𝑥 = 𝐴𝜑))
43eximdv 1912 . 2 (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
51, 4syl5com 31 1 (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1533  wex 1773  wcel 2098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-clel 2802
This theorem is referenced by:  spcedv  3582  spcev  3590  eqeu  3698  absneu  4734  issn  4835  elpreqprlem  4868  elunii  4914  axpweq  5350  brcogw  5871  opeldmd  5909  breldmg  5912  dmsnopg  6219  predtrss  6330  fvrnressn  7170  f1oexbi  7936  unielxp  8032  frrlem13  8304  f1oen4g  8985  f1dom4g  8986  f1oen3g  8987  f1dom3g  8988  f1domg  8993  en2sn  9067  en2snOLD  9068  en2prd  9076  fodomr  9156  ordiso  9546  fowdom  9601  inf0  9651  infeq5i  9666  oncard  9990  cardsn  9999  dfac8b  10061  ac10ct  10064  aceq3lem  10150  dfacacn  10171  cflem  10276  cflecard  10283  cfslb  10296  coftr  10303  alephsing  10306  fin4i  10328  axdc4lem  10485  gchi  10654  hasheqf1oi  14354  relexpindlem  15054  climeu  15543  brcici  17802  initoeu2lem2  18023  gsumval2a  18664  irinitoringc  21439  uptx  23590  alexsubALTlem1  24012  ptcmplem3  24019  prdsxmslem2  24499  tgjustf  28369  tgjustr  28370  wlksnwwlknvbij  29811  clwwlkvbij  30015  aciunf1lem  32549  locfinref  33593  fnimage  35676  fnessref  35992  refssfne  35993  filnetlem4  36016  bj-restb  36724  fin2so  37231  unirep  37338  indexa  37357  nssd  44616  choicefi  44717  axccdom  44739  stoweidlem5  45536  stoweidlem27  45558  stoweidlem28  45559  stoweidlem31  45562  stoweidlem43  45574  stoweidlem44  45575  stoweidlem51  45582  stoweidlem59  45590  nsssmfmbflem  46309  fundcmpsurinjpreimafv  46890  sprbisymrel  46981  uspgrbisymrelALT  47408
  Copyright terms: Public domain W3C validator