Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralsng Structured version   Visualization version   GIF version

Theorem ralsng 4165
 Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
Hypothesis
Ref Expression
ralsng.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ralsng (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem ralsng
StepHypRef Expression
1 ralsnsg 4163 . 2 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑[𝐴 / 𝑥]𝜑))
2 ralsng.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32sbcieg 3435 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
41, 3bitrd 267 1 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  ∀wral 2896  [wsbc 3402  {csn 4125 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-sbc 3403  df-sn 4126 This theorem is referenced by:  2ralsng  4167  ralsn  4169  ralprg  4181  raltpg  4183  ralunsn  4360  iinxsng  4536  frirr  5015  posn  5110  frsn  5112  f12dfv  6429  ranksnb  8573  mgm1  17080  sgrp1  17116  mnd1  17154  grp1  17345  cntzsnval  17580  abl1  18092  srgbinomlem4  18366  ring1  18425  mat1dimmul  20101  ufileu  21533  istrkg3ld  25160  cusgra1v  25990  cusgra2v  25991  dfconngra1  26199  1conngra  26203  wwlknext  26252  clwwlkn2  26303  wwlkext2clwwlk  26331  rusgrasn  26472  frgra1v  26525  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  1hevtxdg0  40720  1wlkp1lem8  40889  wwlksnext  41099  wwlksext2clwwlk  41231  dfconngr1  41355  1conngr  41361  frgr1v  41441  zlidlring  41718  linds0  42048  snlindsntor  42054  lmod1  42075
 Copyright terms: Public domain W3C validator