Theorem ralsng 4620

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2147, ax-12 2185. (Revised by GG, 30-Sep-2024.)

Hypothesis

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

Assertion

Ref	Expression
ralsng	⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

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

Proof of Theorem ralsng

Step	Hyp	Ref	Expression
1		df-ral 3053	. . 3 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑))
2		velsn 4584	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3	2	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑))
4	3	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
5	1, 4	bitri 275	. 2 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
6		elisset 2819	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
7		ralsng.1	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	7	pm5.74i 271	. . . . . 6 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
9	8	albii 1821	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
10	9	a1i 11	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)))
11		19.23v 1944	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
12	11	a1i 11	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)))
13		pm5.5 361	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
14	10, 12, 13	3bitrd 305	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
15	6, 14	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
16	5, 15	bitrid 283	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  {csn 4568

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3432  df-sn 4569

This theorem is referenced by:  rexsng  4621  2ralsng  4623  ralsn  4626  ralprg  4641  raltpg  4643  ralunsn  4838  iinxsng  5031  frirr  5598  posn  5708  frsn  5710  f1ounsn  7218  f12dfv  7219  naddov2  8606  naddunif  8620  naddasslem1  8621  naddasslem2  8622  ranksnb  9740  mgm1  18615  sgrp1  18686  mnd1  18736  grp1  19012  cntzsnval  19288  abl1  19830  srgbinomlem4  20199  ring1  20280  mat1dimmul  22450  ufileu  23893  sltssnb  27780  eqcuts3  27815  bdayn0p1  28380  istrkg3ld  28548  1hevtxdg0  29594  wlkp1lem8  29767  wwlksnext  29981  wwlksext2clwwlk  30147  dfconngr1  30278  1conngr  30284  frgr1v  30361  lindssn  33458  lbslsat  33781  bj-raldifsn  37425  lindsadd  37945  poimirlem26  37978  poimirlem27  37979  poimirlem31  37983  cantnfresb  43767  safesnsupfilb  43860  cfsetsnfsetf1  47504  zlidlring  48707  linds0  48938  snlindsntor  48944  lmod1  48965