Theorem ralsng 4573

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 7-Apr-2023.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

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

Proof of Theorem ralsng

Step	Hyp	Ref	Expression
1		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜓
2		ralsng.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	ralsngf 4571	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-sbc 3721  df-sn 4526

This theorem is referenced by:  2ralsng  4576  ralsn  4579  raltpg  4594  ralunsn  4786  iinxsng  4973  frirr  5496  posn  5601  frsn  5603  f12dfv  7008  ranksnb  9240  mgm1  17860  sgrp1  17902  mnd1  17944  grp1  18198  cntzsnval  18446  abl1  18979  srgbinomlem4  19286  ring1  19348  mat1dimmul  21081  ufileu  22524  istrkg3ld  26255  1hevtxdg0  27295  wlkp1lem8  27470  wwlksnext  27679  wwlksext2clwwlk  27842  dfconngr1  27973  1conngr  27979  frgr1v  28056  lindssn  30993  lbslsat  31102  bj-raldifsn  34515  lindsadd  35050  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  zlidlring  44552  linds0  44874  snlindsntor  44880  lmod1  44901