Theorem spcegv 3516

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507  ∃wex 1742   ∈ wcel 2050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771  df-clel 2846

This theorem is referenced by:  spcev  3525  elabd  3583  eqeu  3611  absneu  4539  issn  4638  elpreqprlem  4671  elunii  4718  axpweq  5119  brcogw  5590  opeldmd  5626  breldmg  5629  dmsnopg  5911  fvrnressn  6748  f1oexbi  7450  unielxp  7541  f1oen3g  8324  f1domg  8328  fodomr  8466  ordiso  8777  fowdom  8832  infeq5i  8895  oncard  9185  cardsn  9194  dfac8b  9253  ac10ct  9256  aceq3lem  9342  dfacacn  9363  cflem  9468  cflecard  9475  cfslb  9488  coftr  9495  alephsing  9498  fin4i  9520  axdc4lem  9677  gchi  9846  hasheqf1oi  13530  relexpindlem  14286  climeu  14776  brcici  16931  initoeu2lem2  17136  gsumval2a  17750  uptx  21940  alexsubALTlem1  22362  ptcmplem3  22369  prdsxmslem2  22845  tgjustf  25964  tgjustr  25965  wlksnwwlknvbij  27411  clwwlkvbij  27644  clwwlkvbijOLD  27645  aciunf1lem  30172  locfinref  30749  frrlem13  32656  fnimage  32911  fnessref  33226  refssfne  33227  filnetlem4  33250  bj-restb  33895  fin2so  34320  unirep  34430  indexa  34450  rp-isfinite5  39279  nssd  40795  choicefi  40889  axccdom  40913  stoweidlem5  41722  stoweidlem27  41744  stoweidlem28  41745  stoweidlem31  41748  stoweidlem43  41760  stoweidlem44  41761  stoweidlem51  41768  stoweidlem59  41776  nsssmfmbflem  42486  sprbisymrel  43030  isomuspgrlem2  43367  uspgrbisymrelALT  43399  irinitoringc  43705