Theorem spcegv 3597

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ∃wex 1780   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

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

This theorem is referenced by:  spcedv  3599  spcev  3607  eqeu  3697  absneu  4664  issn  4763  elpreqprlem  4796  elunii  4843  axpweq  5265  brcogw  5739  opeldmd  5775  breldmg  5778  dmsnopg  6070  fvrnressn  6923  f1oexbi  7633  unielxp  7727  f1oen3g  8525  f1domg  8529  fodomr  8668  ordiso  8980  fowdom  9035  infeq5i  9099  oncard  9389  cardsn  9398  dfac8b  9457  ac10ct  9460  aceq3lem  9546  dfacacn  9567  cflem  9668  cflecard  9675  cfslb  9688  coftr  9695  alephsing  9698  fin4i  9720  axdc4lem  9877  gchi  10046  hasheqf1oi  13713  relexpindlem  14422  climeu  14912  brcici  17070  initoeu2lem2  17275  gsumval2a  17895  uptx  22233  alexsubALTlem1  22655  ptcmplem3  22662  prdsxmslem2  23139  tgjustf  26259  tgjustr  26260  wlksnwwlknvbij  27687  clwwlkvbij  27892  aciunf1lem  30407  locfinref  31105  frrlem13  33135  fnimage  33390  fnessref  33705  refssfne  33706  filnetlem4  33729  bj-restb  34388  fin2so  34894  unirep  35003  indexa  35023  rp-isfinite5  39903  nssd  41391  choicefi  41483  axccdom  41507  stoweidlem5  42310  stoweidlem27  42332  stoweidlem28  42333  stoweidlem31  42336  stoweidlem43  42348  stoweidlem44  42349  stoweidlem51  42356  stoweidlem59  42364  nsssmfmbflem  43074  fundcmpsurinjpreimafv  43588  sprbisymrel  43681  isomuspgrlem2  44018  uspgrbisymrelALT  44050  irinitoringc  44360