Theorem rexsng 4410

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

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

Proof of Theorem rexsng

Step	Hyp	Ref	Expression
1		rexsns 4408	. 2 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)
2		ralsng.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	sbcieg 3666	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
4	1, 3	syl5bb 275	1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1653   ∈ wcel 2157  ∃wrex 3090  [wsbc 3633  {csn 4368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rex 3095  df-v 3387  df-sbc 3634  df-sn 4369

This theorem is referenced by:  rexsn  4414  rexprg  4425  rextpg  4427  iunxsng  4792  frirr  5289  frsn  5394  imasng  5704  scshwfzeqfzo  13911  dvdsprmpweqnn  15922  mnd1  17646  grp1  17838  1loopgrvd0  26754  1egrvtxdg0  26761  nfrgr2v  27621  1vwmgr  27625  ballotlemfc0  31071  ballotlemfcc  31072  bj-restsn  33528  elpaddat  35825  elpadd2at  35827  brfvidRP  38763  iccelpart  42209  zlidlring  42727  lco0  43015