Theorem ralsng 4636

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 2178, ax-12 2213. (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 3078	. . 3 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑))
2		velsn 4600	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3	2	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑))
4	3	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
5	1, 4	bitri 278	. 2 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
6		elisset 2843	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
7		ralsng.1	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	7	pm5.74i 274	. . . . . 6 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
9	8	albii 1852	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
10	9	a1i 11	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)))
11		19.23v 1975	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
12	11	a1i 11	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)))
13		pm5.5 364	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
14	10, 12, 13	3bitrd 308	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
15	6, 14	syl 18	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
16	5, 15	bitrid 286	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∀wral 3077  {csn 4584

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-sn 4585

This theorem is used by:  rexsng  4637  2ralsng  4639  ralsn  4642  ralprg  4657  raltpg  4659  ralunsn  4854  iinxsng  5048  frirr  5627  posn  5737  frsn  5739  f1ounsn  7272  f12dfv  7273  naddov2  8672  naddunif  8687  naddasslem1  8688  naddasslem2  8689  ranksnb  9818  mgm1  18816  sgrp1  18898  mnd1  18953  grp1  19237  cntzsnval  19518  abl1  20060  srgbinomlem4  20435  ring1  20521  mat1dimmul  22771  ufileu  24218  sltssnb  28137  eqcuts3  28172  bdayn0p1  28737  istrkg3ld  28905  1hevtxdg0  30068  wlkp1lem8  30241  wwlksnext  30464  wwlksext2clwwlk  30630  dfconngr1  30771  1conngr  30777  frgr1v  30854  lindssn  33915  lbslsat  34230  bj-raldifsn  37989  lindsadd  38504  poimirlem26  38532  poimirlem27  38533  poimirlem31  38537  cantnfresb  44284  safesnsupfilb  44377  cfsetsnfsetf1  48073  zlidlring  49275  linds0  49521  snlindsntor  49527  lmod1  49548