Theorem rexsng 4644

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2179, ax-12 2216. (Revised by GG, 30-Sep-2024.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

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

Proof of Theorem rexsng

Step	Hyp	Ref	Expression
1		ralsng.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	notbid 321	. . 3 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	ralsng 4643	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓))
4		dfrex2 3094	. . 3 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ ¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑)
5		bicom1 224	. . . 4 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜓 ↔ ∀𝑥 ∈ {𝐴} ¬ 𝜑))
6	5	con1bid 358	. . 3 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ 𝜓))
7	4, 6	bitrid 286	. 2 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
8	3, 7	syl 18	1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-sn 4592

This theorem is used by:  rexsn  4650  rextpg  4667  iunxsng  5058  frirr  5639  frsn  5751  imasng  6088  naddunif  8682  snecg  8777  scshwfzeqfzo  14883  dvdsprmpweqnn  16963  mnd1  18861  grp1  19137  pzriprnglem3  21663  pzriprnglem10  21670  psdmul  22359  cutmax  28158  cutmin  28159  halfcut  28682  elntg2  29366  1loopgrvd0  29888  1egrvtxdg0  29895  nfrgr2v  30670  1vwmgr  30674  elgrplsmsn  33743  grplsmid  33753  dflringlem  33824  ballotlemfc0  34924  ballotlemfcc  34925  bj-restsn  37757  elrnressn  38962  elpaddat  40611  elpadd2at  40613  brfvidRP  44447  mnuunid  45020  iccelpart  48215  zlidlring  49032  lco0  49240