Theorem ralsng 4674

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 2140, ax-12 2176. (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 3061	. . 3 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑))
2		velsn 4641	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3	2	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑))
4	3	albii 1818	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
5	1, 4	bitri 275	. 2 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))
6		elisset 2822	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
7		ralsng.1	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	7	pm5.74i 271	. . . . . 6 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
9	8	albii 1818	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
10	9	a1i 11	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)))
11		19.23v 1941	. . . . 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 1537   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ∀wral 3060  {csn 4625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-v 3481  df-sn 4626

This theorem is referenced by:  rexsng  4675  2ralsng  4677  ralsn  4680  ralprg  4695  raltpg  4697  ralunsn  4893  iinxsng  5087  frirr  5660  posn  5770  frsn  5772  f1ounsn  7293  f12dfv  7294  naddov2  8718  naddunif  8732  naddasslem1  8733  naddasslem2  8734  ranksnb  9868  mgm1  18672  sgrp1  18743  mnd1  18793  grp1  19066  cntzsnval  19343  abl1  19885  srgbinomlem4  20227  ring1  20308  mat1dimmul  22483  ufileu  23928  istrkg3ld  28470  1hevtxdg0  29524  wlkp1lem8  29699  wwlksnext  29914  wwlksext2clwwlk  30077  dfconngr1  30208  1conngr  30214  frgr1v  30291  lindssn  33407  lbslsat  33668  bj-raldifsn  37102  lindsadd  37621  poimirlem26  37654  poimirlem27  37655  poimirlem31  37659  cantnfresb  43342  safesnsupfilb  43436  cfsetsnfsetf1  47076  zlidlring  48155  linds0  48387  snlindsntor  48393  lmod1  48414