Theorem rexsng 4364

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 4362	. 2 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)
2		ralsng.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	sbcieg 3610	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
4	1, 3	syl5bb 272	1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2140  ∃wrex 3052  [wsbc 3577  {csn 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rex 3057  df-v 3343  df-sbc 3578  df-sn 4323

This theorem is referenced by:  rexsn  4368  rexprg  4380  rextpg  4382  iunxsng  4755  frirr  5244  frsn  5347  imasng  5646  scshwfzeqfzo  13793  dvdsprmpweqnn  15812  mnd1  17553  grp1  17744  1loopgrvd0  26632  1egrvtxdg0  26639  nfrgr2v  27448  1vwmgr  27452  ballotlemfc0  30885  ballotlemfcc  30886  bj-restsn  33360  elpaddat  35612  elpadd2at  35614  brfvidRP  38501  iccelpart  41898  zlidlring  42457  lco0  42745