Theorem rexsng 4574

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Proof shortened by AV, 7-Apr-2023.)

Hypothesis

Ref	Expression
ralsng.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rexsng	⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem rexsng

Step	Hyp	Ref	Expression
1		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜓
2		ralsng.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rexsngf 4570	1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∃wrex 3107  {csn 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rex 3112  df-v 3443  df-sbc 3721  df-sn 4526

This theorem is referenced by:  rexsn  4580  rextpg  4595  iunxsng  4975  frirr  5496  frsn  5603  imasng  5918  scshwfzeqfzo  14179  dvdsprmpweqnn  16211  mnd1  17944  grp1  18198  elntg2  26779  1loopgrvd0  27294  1egrvtxdg0  27301  nfrgr2v  28057  1vwmgr  28061  elgrplsmsn  30998  ballotlemfc0  31860  ballotlemfcc  31861  bj-restsn  34497  elpaddat  37100  elpadd2at  37102  brfvidRP  40389  mnuunid  40985  iccelpart  43950  zlidlring  44552  lco0  44836