Theorem ralsng 4606

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 2139, ax-12 2173. (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 3068	. . 3 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑))
2		velsn 4574	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3	2	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑))
4	3	albii 1823	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
5	1, 4	bitri 274	. 2 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
6		elisset 2820	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
7		ralsng.1	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	7	pm5.74i 270	. . . . . 6 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
9	8	albii 1823	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
10	9	a1i 11	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)))
11		19.23v 1946	. . . . 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	syl5bb 282	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∀wral 3063  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-sn 4559

This theorem is referenced by:  rexsng  4607  2ralsng  4609  ralsn  4614  ralprg  4627  raltpg  4631  ralunsn  4822  iinxsng  5013  frirr  5557  posn  5663  frsn  5665  f12dfv  7126  ranksnb  9516  mgm1  18257  sgrp1  18299  mnd1  18341  grp1  18597  cntzsnval  18845  abl1  19382  srgbinomlem4  19694  ring1  19756  mat1dimmul  21533  ufileu  22978  istrkg3ld  26726  1hevtxdg0  27775  wlkp1lem8  27950  wwlksnext  28159  wwlksext2clwwlk  28322  dfconngr1  28453  1conngr  28459  frgr1v  28536  lindssn  31475  lbslsat  31601  naddov2  33761  bj-raldifsn  35198  lindsadd  35697  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  cfsetsnfsetf1  44440  zlidlring  45374  linds0  45694  snlindsntor  45700  lmod1  45721