Theorem spcegv 3551

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-clel 2835

This theorem is used by:  spcedv  3552  spcev  3560  eqeu  3664  absneu  4689  issn  4792  elpreqprlem  4826  elunii  4872  axpweq  5315  brcogw  5848  opeldmd  5890  breldmg  5893  dmsnopg  6209  predtrss  6320  fvrnressn  7159  f1oexbi  7926  unielxp  8025  frrlem13  8298  f1oen4g  8973  f1dom4g  8974  f1oen3g  8975  f1dom3g  8976  f1domg  8980  en2sn  9051  en2prd  9057  fodomr  9129  fodomfir  9300  ordiso  9491  fowdom  9546  inf0  9603  infeq5i  9618  oncard  9968  cardsn  9977  dfac8b  10037  ac10ct  10040  aceq3lem  10126  dfacacn  10147  cflem  10250  cflecard  10257  cfslb  10271  coftr  10278  alephsing  10281  fin4i  10303  axdc4lem  10460  gchi  10636  hasheqf1oi  14418  relexpindlem  15139  climeu  15645  brcici  17892  initoeu2lem2  18107  gsumval2a  18790  irinitoringc  21695  uptx  23854  alexsubALTlem1  24276  ptcmplem3  24283  prdsxmslem2  24758  tgjustf  28817  tgjustr  28818  wlksnwwlknvbij  30379  clwwlkvbij  30586  aciunf1lem  33138  locfinref  34354  tz9.1regs  35663  fnimage  36509  fnessref  36979  refssfne  36980  filnetlem4  37003  dfttc3gw  37145  bj-restb  37847  fin2so  38364  unirep  38467  indexa  38486  nssd  45940  choicefi  46034  axccdom  46055  stoweidlem5  46836  stoweidlem27  46858  stoweidlem28  46859  stoweidlem31  46862  stoweidlem43  46874  stoweidlem44  46875  stoweidlem51  46882  stoweidlem59  46890  nsssmfmbflem  47609  fundcmpsurinjpreimafv  48311  sprbisymrel  48402  uspgrbisymrelALT  49074