Theorem ralsng 4677

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 2137, ax-12 2171. (Revised by Gino Giotto, 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 3062	. . 3 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑))
2		velsn 4644	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3	2	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑))
4	3	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
5	1, 4	bitri 274	. 2 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
6		elisset 2815	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
7		ralsng.1	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	7	pm5.74i 270	. . . . . 6 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
9	8	albii 1821	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
10	9	a1i 11	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)))
11		19.23v 1945	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
12	11	a1i 11	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)))
13		pm5.5 361	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
14	10, 12, 13	3bitrd 304	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
15	6, 14	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
16	5, 15	bitrid 282	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∀wral 3061  {csn 4628

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-sn 4629

This theorem is referenced by:  rexsng  4678  2ralsng  4680  ralsn  4685  ralprg  4698  raltpg  4702  ralunsn  4894  iinxsng  5091  frirr  5653  posn  5761  frsn  5763  f12dfv  7273  naddov2  8680  naddunif  8694  naddasslem1  8695  naddasslem2  8696  ranksnb  9824  mgm1  18583  sgrp1  18654  mnd1  18701  grp1  18966  cntzsnval  19229  abl1  19775  srgbinomlem4  20123  ring1  20198  mat1dimmul  22198  ufileu  23643  istrkg3ld  27967  1hevtxdg0  29017  wlkp1lem8  29192  wwlksnext  29402  wwlksext2clwwlk  29565  dfconngr1  29696  1conngr  29702  frgr1v  29779  lindssn  32756  lbslsat  32977  bj-raldifsn  36284  lindsadd  36784  poimirlem26  36817  poimirlem27  36818  poimirlem31  36822  cantnfresb  42376  safesnsupfilb  42471  cfsetsnfsetf1  46068  zlidlring  46915  linds0  47234  snlindsntor  47240  lmod1  47261