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

Theorem ralsng 4209
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 4207 . 2 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑[𝐴 / 𝑥]𝜑))
2 ralsng.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32sbcieg 3462 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
41, 3bitrd 268 1 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988  wral 2909  [wsbc 3429  {csn 4168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-v 3197  df-sbc 3430  df-sn 4169
This theorem is referenced by:  2ralsng  4211  ralsn  4213  ralprg  4225  raltpg  4227  ralunsn  4413  iinxsng  4591  frirr  5081  posn  5177  frsn  5179  f12dfv  6514  ranksnb  8675  mgm1  17238  sgrp1  17274  mnd1  17312  grp1  17503  cntzsnval  17738  abl1  18250  srgbinomlem4  18524  ring1  18583  mat1dimmul  20263  ufileu  21704  istrkg3ld  25341  1hevtxdg0  26382  wlkp1lem8  26558  wwlksnext  26769  wwlksext2clwwlk  26904  dfconngr1  27028  1conngr  27034  frgr1v  27115  poimirlem26  33406  poimirlem27  33407  poimirlem31  33411  zlidlring  41693  linds0  42019  snlindsntor  42025  lmod1  42046
  Copyright terms: Public domain W3C validator