Theorem spcegv 3555

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1811   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-clel 2839

This theorem is used by:  spcedv  3556  spcev  3564  eqeu  3667  absneu  4689  issn  4790  elpreqprlem  4824  elunii  4875  axpweq  5316  brcogw  5851  opeldmd  5893  breldmg  5896  dmsnopg  6221  predtrss  6332  fvrnressn  7176  f1oexbi  7950  unielxp  8049  frrlem13  8330  f1oen4g  9005  f1dom4g  9006  f1oen3g  9007  f1dom3g  9008  f1domg  9012  en2sn  9083  en2prd  9089  fodomr  9161  fodomfir  9333  ordiso  9523  fowdom  9578  inf0  9635  infeq5i  9650  oncard  10054  cardsn  10063  dfac8b  10123  ac10ct  10126  aceq3lem  10212  dfacacn  10233  cflem  10336  cflecard  10343  cfslb  10357  coftr  10364  alephsing  10367  fin4i  10389  axdc4lem  10546  gchi  10722  hasheqf1oi  14508  relexpindlem  15231  climeu  15737  brcici  17990  initoeu2lem2  18205  gsumval2a  18889  irinitoringc  21800  uptx  23959  alexsubALTlem1  24381  ptcmplem3  24388  prdsxmslem2  24863  tgjustf  28950  tgjustr  28951  wlksnwwlknvbij  30512  clwwlkvbij  30719  aciunf1lem  33313  locfinref  34529  tz9.1regs  35876  fnimage  36821  fnessref  37275  refssfne  37276  filnetlem4  37299  dfttc3gw  37441  bj-restb  38157  fin2so  38673  unirep  38791  indexa  38810  nssd  46262  choicefi  46356  axccdom  46377  stoweidlem5  47157  stoweidlem27  47179  stoweidlem28  47180  stoweidlem31  47183  stoweidlem43  47195  stoweidlem44  47196  stoweidlem51  47203  stoweidlem59  47211  nsssmfmbflem  47930  fundcmpsurinjpreimafv  48632  sprbisymrel  48723  uspgrbisymrelALT  49395