Theorem spcegv 3537

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-clel 2817

This theorem is referenced by:  spcedv  3538  spcev  3546  eqeu  3642  absneu  4665  issn  4764  elpreqprlem  4797  elunii  4845  axpweq  5288  brcogw  5780  opeldmd  5818  breldmg  5821  dmsnopg  6121  predtrss  6229  fvrnressn  7042  f1oexbi  7784  unielxp  7878  frrlem13  8123  f1oen3g  8763  f1dom3g  8764  f1domg  8769  en2sn  8840  en2snOLD  8841  fodomr  8924  ordiso  9284  fowdom  9339  inf0  9388  infeq5i  9403  oncard  9727  cardsn  9736  dfac8b  9796  ac10ct  9799  aceq3lem  9885  dfacacn  9906  cflem  10011  cflecard  10018  cfslb  10031  coftr  10038  alephsing  10041  fin4i  10063  axdc4lem  10220  gchi  10389  hasheqf1oi  14075  relexpindlem  14783  climeu  15273  brcici  17521  initoeu2lem2  17739  gsumval2a  18378  uptx  22785  alexsubALTlem1  23207  ptcmplem3  23214  prdsxmslem2  23694  tgjustf  26843  tgjustr  26844  wlksnwwlknvbij  28282  clwwlkvbij  28486  aciunf1lem  31008  locfinref  31800  fnimage  34240  fnessref  34555  refssfne  34556  filnetlem4  34579  bj-restb  35274  fin2so  35773  unirep  35880  indexa  35900  rp-isfinite5  41131  nssd  42662  choicefi  42747  axccdom  42769  stoweidlem5  43553  stoweidlem27  43575  stoweidlem28  43576  stoweidlem31  43579  stoweidlem43  43591  stoweidlem44  43592  stoweidlem51  43599  stoweidlem59  43607  nsssmfmbflem  44323  fundcmpsurinjpreimafv  44871  sprbisymrel  44962  isomuspgrlem2  45296  uspgrbisymrelALT  45328  irinitoringc  45638