Theorem spcegv 3597

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2139, ax-11 2155. (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

Step	Hyp	Ref	Expression
1		elisset 2821	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		spcgv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	biimprcd 250	. . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
4	3	eximdv 1915	. 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
5	1, 4	syl5com 31	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wex 1776   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-clel 2814

This theorem is referenced by:  spcedv  3598  spcev  3606  eqeu  3715  absneu  4733  issn  4837  elpreqprlem  4871  elunii  4917  axpweq  5357  brcogw  5882  opeldmd  5920  breldmg  5923  dmsnopg  6235  predtrss  6345  fvrnressn  7181  f1oexbi  7951  unielxp  8051  frrlem13  8322  f1oen4g  9004  f1dom4g  9005  f1oen3g  9006  f1dom3g  9007  f1domg  9011  en2sn  9080  en2prd  9087  fodomr  9167  fodomfir  9366  ordiso  9554  fowdom  9609  inf0  9659  infeq5i  9674  oncard  9998  cardsn  10007  dfac8b  10069  ac10ct  10072  aceq3lem  10158  dfacacn  10180  cflem  10283  cflemOLD  10284  cflecard  10291  cfslb  10304  coftr  10311  alephsing  10314  fin4i  10336  axdc4lem  10493  gchi  10662  hasheqf1oi  14387  relexpindlem  15099  climeu  15588  brcici  17848  initoeu2lem2  18069  gsumval2a  18711  irinitoringc  21508  uptx  23649  alexsubALTlem1  24071  ptcmplem3  24078  prdsxmslem2  24558  tgjustf  28496  tgjustr  28497  wlksnwwlknvbij  29938  clwwlkvbij  30142  aciunf1lem  32679  locfinref  33802  fnimage  35911  fnessref  36340  refssfne  36341  filnetlem4  36364  bj-restb  37077  fin2so  37594  unirep  37701  indexa  37720  nssd  45045  choicefi  45143  axccdom  45165  stoweidlem5  45961  stoweidlem27  45983  stoweidlem28  45984  stoweidlem31  45987  stoweidlem43  45999  stoweidlem44  46000  stoweidlem51  46007  stoweidlem59  46015  nsssmfmbflem  46734  fundcmpsurinjpreimafv  47333  sprbisymrel  47424  uspgrbisymrelALT  47999