Theorem rexsng 4636

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2142, ax-12 2178. (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 318	. . 3 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	ralsng 4635	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓))
4		dfrex2 3056	. . 3 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ ¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑)
5		bicom1 221	. . . 4 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜓 ↔ ∀𝑥 ∈ {𝐴} ¬ 𝜑))
6	5	con1bid 355	. . 3 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ 𝜓))
7	4, 6	bitrid 283	. 2 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
8	3, 7	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3446  df-sn 4586

This theorem is referenced by:  rexsn  4642  rextpg  4659  iunxsng  5049  frirr  5607  frsn  5719  imasng  6044  naddunif  8634  scshwfzeqfzo  14768  dvdsprmpweqnn  16832  mnd1  18682  grp1  18955  pzriprnglem3  21369  pzriprnglem10  21376  psdmul  22029  cutmax  27818  cutmin  27819  halfcut  28309  elntg2  28888  1loopgrvd0  29408  1egrvtxdg0  29415  nfrgr2v  30174  1vwmgr  30178  elgrplsmsn  33334  grplsmid  33348  ballotlemfc0  34457  ballotlemfcc  34458  bj-restsn  37043  elrnressn  38235  elpaddat  39771  elpadd2at  39773  brfvidRP  43650  mnuunid  44239  iccelpart  47407  zlidlring  48195  lco0  48389