Theorem spcegv 3535

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

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ∃wex 1786   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-clel 2818

This theorem is referenced by:  spcedv  3536  spcev  3544  eqeu  3645  absneu  4670  issn  4769  elpreqprlem  4802  elunii  4850  axpweq  5291  brcogw  5776  opeldmd  5814  breldmg  5817  dmsnopg  6115  predtrss  6224  fvrnressn  7030  f1oexbi  7769  unielxp  7862  frrlem13  8105  f1oen3g  8737  f1dom3g  8738  f1domg  8743  en2sn  8814  en2snOLD  8815  fodomr  8897  ordiso  9253  fowdom  9308  inf0  9357  infeq5i  9372  oncard  9719  cardsn  9728  dfac8b  9788  ac10ct  9791  aceq3lem  9877  dfacacn  9898  cflem  10003  cflecard  10010  cfslb  10023  coftr  10030  alephsing  10033  fin4i  10055  axdc4lem  10212  gchi  10381  hasheqf1oi  14064  relexpindlem  14772  climeu  15262  brcici  17510  initoeu2lem2  17728  gsumval2a  18367  uptx  22774  alexsubALTlem1  23196  ptcmplem3  23203  prdsxmslem2  23683  tgjustf  26832  tgjustr  26833  wlksnwwlknvbij  28269  clwwlkvbij  28473  aciunf1lem  30995  locfinref  31787  fnimage  34227  fnessref  34542  refssfne  34543  filnetlem4  34566  bj-restb  35261  fin2so  35760  unirep  35867  indexa  35887  rp-isfinite5  41103  nssd  42625  choicefi  42710  axccdom  42732  stoweidlem5  43517  stoweidlem27  43539  stoweidlem28  43540  stoweidlem31  43543  stoweidlem43  43555  stoweidlem44  43556  stoweidlem51  43563  stoweidlem59  43571  nsssmfmbflem  44281  fundcmpsurinjpreimafv  44829  sprbisymrel  44920  isomuspgrlem2  45254  uspgrbisymrelALT  45286  irinitoringc  45596