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

Theorem spcegv 3545
 Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2142, ax-11 2158. (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 3452 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 spcgv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
32biimprcd 253 . . 3 (𝜓 → (𝑥 = 𝐴𝜑))
43eximdv 1918 . 2 (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
51, 4syl5com 31 1 (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2111 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870 This theorem is referenced by:  spcedv  3547  spcev  3555  eqeu  3645  absneu  4624  issn  4723  elpreqprlem  4756  elunii  4806  axpweq  5231  brcogw  5704  opeldmd  5740  breldmg  5743  dmsnopg  6038  fvrnressn  6901  f1oexbi  7618  unielxp  7712  f1oen3g  8511  f1domg  8515  fodomr  8655  ordiso  8967  fowdom  9022  inf0  9071  infeq5i  9086  oncard  9376  cardsn  9385  dfac8b  9445  ac10ct  9448  aceq3lem  9534  dfacacn  9555  cflem  9660  cflecard  9667  cfslb  9680  coftr  9687  alephsing  9690  fin4i  9712  axdc4lem  9869  gchi  10038  hasheqf1oi  13711  relexpindlem  14417  climeu  14907  brcici  17065  initoeu2lem2  17270  gsumval2a  17890  uptx  22240  alexsubALTlem1  22662  ptcmplem3  22669  prdsxmslem2  23146  tgjustf  26277  tgjustr  26278  wlksnwwlknvbij  27704  clwwlkvbij  27908  aciunf1lem  30435  locfinref  31209  frrlem13  33263  fnimage  33518  fnessref  33833  refssfne  33834  filnetlem4  33857  bj-restb  34528  fin2so  35063  unirep  35170  indexa  35190  rp-isfinite5  40268  nssd  41784  choicefi  41872  axccdom  41896  stoweidlem5  42690  stoweidlem27  42712  stoweidlem28  42713  stoweidlem31  42716  stoweidlem43  42728  stoweidlem44  42729  stoweidlem51  42736  stoweidlem59  42744  nsssmfmbflem  43454  fundcmpsurinjpreimafv  43968  sprbisymrel  44059  isomuspgrlem2  44394  uspgrbisymrelALT  44426  irinitoringc  44736
 Copyright terms: Public domain W3C validator