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

Theorem ralsng 4409
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 4407 . 2 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑[𝐴 / 𝑥]𝜑))
2 ralsng.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32sbcieg 3666 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
41, 3bitrd 271 1 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1653  wcel 2157  wral 3089  [wsbc 3633  {csn 4368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-v 3387  df-sbc 3634  df-sn 4369
This theorem is referenced by:  2ralsng  4411  ralsn  4413  ralprg  4424  raltpg  4426  ralunsn  4614  iinxsng  4790  frirr  5289  posn  5392  frsn  5394  f12dfv  6757  ranksnb  8940  mgm1  17572  sgrp1  17608  mnd1  17646  grp1  17838  cntzsnval  18069  abl1  18584  srgbinomlem4  18859  ring1  18918  mat1dimmul  20608  ufileu  22051  istrkg3ld  25712  1hevtxdg0  26755  wlkp1lem8  26933  wwlksnext  27162  wwlksext2clwwlk  27373  wwlksext2clwwlkOLD  27374  dfconngr1  27532  1conngr  27538  frgr1v  27620  poimirlem26  33924  poimirlem27  33925  poimirlem31  33929  zlidlring  42727  linds0  43053  snlindsntor  43059  lmod1  43080
  Copyright terms: Public domain W3C validator