Theorem ralsn 4638

Description: Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)

Hypotheses

Ref	Expression
ralsn.1	⊢ 𝐴 ∈ V
ralsn.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralsn	⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ralsn

Step	Hyp	Ref	Expression
1		ralsn.1	. 2 ⊢ 𝐴 ∈ V
2		ralsn.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	ralsng 4632	. 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∀wral 3076  Vcvv 3450  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-sn 4585

This theorem is used by:  xpord2indlem  8166  xpord3inddlem  8173  naddcllem  8688  naddasslem1  8707  naddasslem2  8708  elixpsn  8968  frfi  9279  dffi3  9426  ssttrcl  9719  ttrclss  9724  ttrclselem2  9730  fseqenlem1  10106  fpwwe2lem12  10730  hashbc  14601  hashf1lem1  14603  eqs1  14764  cshw1  14977  rpnnen2lem11  16397  drsdirfi  18484  0subg  19367  0subgALT  19787  efgsp1  19956  dprd2da  20263  lbsextlem4  21444  rnglidl0  21514  lindsenlbs  22162  ply1coe  22621  mat0dimcrng  22790  txkgen  23976  xkoinjcn  24011  isufil2  24232  ust0  24544  prdsxmetlem  24692  prdsbl  24815  finiunmbl  25870  xrlimcnp  27301  chtub  27544  2sqlem10  27760  dchrisum0flb  27842  pntpbnd1  27918  conway  28170  etaslts  28184  lesrec  28190  bday1  28205  madebdaylemlrcut  28290  precsexlem9  28606  oncutlt  28655  oniso  28662  n0fincut  28746  bdayn0p1  28760  zcuts  28798  twocut  28814  halfcut  28849  addhalfcut  28850  pw2cut2  28853  1reno  28888  usgr1e  29831  nbgr2vtx1edg  29936  nbuhgr2vtx1edgb  29938  wlkl1loop  30223  crctcshwlkn0lem7  30410  2pthdlem1  30524  rusgrnumwwlkl1  30565  clwwlkccatlem  30585  clwwlkn2  30640  clwwlkel  30642  clwwlkwwlksb  30650  1wlkdlem4  30736  h1deoi  32156  selvply1rhmlemb  34197  vieta  34258  bnj149  35551  subfacp1lem5  36035  cvmlift2lem1  36153  cvmlift2lem12  36165  nmulrid  37038  poimirlem28  38659  poimirlem32  38663  heibor1lem  38836  nadd1suc  44487  nregmodel  46100  usgrexmpl1lem  49212  usgrexmpl2lem  49217  isinito2lem  50726  setc1onsubc  50833