Theorem spcegv 3596

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533  ∃wex 1776   ∈ wcel 2110

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893

This theorem is referenced by:  spcedv  3598  spcev  3606  eqeu  3696  absneu  4663  issn  4762  elpreqprlem  4795  elunii  4842  axpweq  5264  brcogw  5738  opeldmd  5774  breldmg  5777  dmsnopg  6069  fvrnressn  6922  f1oexbi  7632  unielxp  7726  f1oen3g  8524  f1domg  8528  fodomr  8667  ordiso  8979  fowdom  9034  infeq5i  9098  oncard  9388  cardsn  9397  dfac8b  9456  ac10ct  9459  aceq3lem  9545  dfacacn  9566  cflem  9667  cflecard  9674  cfslb  9687  coftr  9694  alephsing  9697  fin4i  9719  axdc4lem  9876  gchi  10045  hasheqf1oi  13711  relexpindlem  14421  climeu  14911  brcici  17069  initoeu2lem2  17274  gsumval2a  17894  uptx  22232  alexsubALTlem1  22654  ptcmplem3  22661  prdsxmslem2  23138  tgjustf  26258  tgjustr  26259  wlksnwwlknvbij  27686  clwwlkvbij  27891  aciunf1lem  30406  locfinref  31105  frrlem13  33135  fnimage  33390  fnessref  33705  refssfne  33706  filnetlem4  33729  bj-restb  34384  fin2so  34878  unirep  34987  indexa  35007  rp-isfinite5  39881  nssd  41369  choicefi  41461  axccdom  41485  stoweidlem5  42289  stoweidlem27  42311  stoweidlem28  42312  stoweidlem31  42315  stoweidlem43  42327  stoweidlem44  42328  stoweidlem51  42335  stoweidlem59  42343  nsssmfmbflem  43053  fundcmpsurinjpreimafv  43567  sprbisymrel  43660  isomuspgrlem2  43997  uspgrbisymrelALT  44029  irinitoringc  44339