Theorem spcegv 3588

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2135, ax-11 2152. (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 2813	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		spcgv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	biimprcd 249	. . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
4	3	eximdv 1918	. 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
5	1, 4	syl5com 31	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wex 1779   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2808

This theorem is referenced by:  spcedv  3589  spcev  3597  eqeu  3703  absneu  4733  issn  4834  elpreqprlem  4867  elunii  4914  axpweq  5349  brcogw  5869  opeldmd  5907  breldmg  5910  dmsnopg  6213  predtrss  6324  fvrnressn  7162  f1oexbi  7923  unielxp  8017  frrlem13  8287  f1oen4g  8964  f1dom4g  8965  f1oen3g  8966  f1dom3g  8967  f1domg  8972  en2sn  9045  en2snOLD  9046  en2prd  9052  fodomr  9132  ordiso  9515  fowdom  9570  inf0  9620  infeq5i  9635  oncard  9959  cardsn  9968  dfac8b  10030  ac10ct  10033  aceq3lem  10119  dfacacn  10140  cflem  10245  cflecard  10252  cfslb  10265  coftr  10272  alephsing  10275  fin4i  10297  axdc4lem  10454  gchi  10623  hasheqf1oi  14317  relexpindlem  15016  climeu  15505  brcici  17753  initoeu2lem2  17971  gsumval2a  18612  uptx  23351  alexsubALTlem1  23773  ptcmplem3  23780  prdsxmslem2  24260  tgjustf  27989  tgjustr  27990  wlksnwwlknvbij  29427  clwwlkvbij  29631  aciunf1lem  32152  locfinref  33117  fnimage  35203  fnessref  35547  refssfne  35548  filnetlem4  35571  bj-restb  36280  fin2so  36780  unirep  36887  indexa  36906  nssd  44097  choicefi  44199  axccdom  44221  stoweidlem5  45021  stoweidlem27  45043  stoweidlem28  45044  stoweidlem31  45047  stoweidlem43  45059  stoweidlem44  45060  stoweidlem51  45067  stoweidlem59  45075  nsssmfmbflem  45794  fundcmpsurinjpreimafv  46376  sprbisymrel  46467  isomuspgrlem2  46801  uspgrbisymrelALT  46833  irinitoringc  47057