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

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

Proof of Theorem ralsng
StepHypRef Expression
1 nfv 1906 . 2 𝑥𝜓
2 ralsng.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2ralsngf 4603 1 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  wral 3135  {csn 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-v 3494  df-sbc 3770  df-sn 4558
This theorem is referenced by:  2ralsng  4608  ralsn  4611  raltpg  4626  ralunsn  4816  iinxsng  5001  frirr  5525  posn  5630  frsn  5632  f12dfv  7021  ranksnb  9244  mgm1  17856  sgrp1  17898  mnd1  17940  grp1  18144  cntzsnval  18392  abl1  18915  srgbinomlem4  19222  ring1  19281  mat1dimmul  21013  ufileu  22455  istrkg3ld  26174  1hevtxdg0  27214  wlkp1lem8  27389  wwlksnext  27598  wwlksext2clwwlk  27763  dfconngr1  27894  1conngr  27900  frgr1v  27977  lindssn  30866  lbslsat  30913  bj-raldifsn  34286  lindsadd  34766  poimirlem26  34799  poimirlem27  34800  poimirlem31  34804  zlidlring  44127  linds0  44448  snlindsntor  44454  lmod1  44475
  Copyright terms: Public domain W3C validator