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

Theorem ralsng 4164
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 4162 . 2 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑[𝐴 / 𝑥]𝜑))
2 ralsng.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32sbcieg 3434 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
41, 3bitrd 266 1 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  wral 2895  [wsbc 3401  {csn 4124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-v 3174  df-sbc 3402  df-sn 4125
This theorem is referenced by:  2ralsng  4166  ralsn  4168  ralprg  4180  raltpg  4182  ralunsn  4354  iinxsng  4530  frirr  5005  posn  5100  frsn  5102  f12dfv  6407  ranksnb  8550  mgm1  17026  sgrp1  17062  mnd1  17100  grp1  17291  cntzsnval  17526  abl1  18038  srgbinomlem4  18312  ring1  18371  mat1dimmul  20043  ufileu  21475  istrkg3ld  25077  cusgra1v  25756  cusgra2v  25757  dfconngra1  25965  1conngra  25969  wwlknext  26018  clwwlkn2  26069  wwlkext2clwwlk  26097  rusgrasn  26238  frgra1v  26291  poimirlem26  32408  poimirlem27  32409  poimirlem31  32413  1hevtxdg0  40722  1wlkp1lem8  40891  wwlksnext  41101  wwlksext2clwwlk  41233  dfconngr1  41357  1conngr  41363  frgr1v  41443  zlidlring  41720  linds0  42050  snlindsntor  42056  lmod1  42077
  Copyright terms: Public domain W3C validator