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

Theorem ralsng 4064
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:   ,   ,

Proof of Theorem ralsng
StepHypRef Expression
1 ralsnsg 4061 . 2
2 ralsng.1 . . 3
32sbcieg 3360 . 2
41, 3bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  A.wral 2807  [.wsbc 3327  {csn 4029
This theorem is referenced by:  2ralsng  4066  ralsn  4068  ralprg  4078  raltpg  4080  ralunsn  4237  iinxsng  4407  frirr  4861  posn  5073  frsn  5075  f12dfv  6179  ranksnb  8266  wrdeqswrdlsw  12674  mgm1  15884  sgrp1  15918  mnd1  15961  mnd1OLD  15962  grp1  16142  cntzsnval  16362  abl1  16872  srgbinomlem4  17194  ring1  17248  mat1dimmul  18978  ufileu  20420  cusgra1v  24461  cusgra2v  24462  dfconngra1  24671  1conngra  24675  wwlknext  24724  clwwlkn2  24775  wwlkext2clwwlk  24803  rusgrasn  24945  frgra1v  24998  zlidlring  32734  linds0  33066  snlindsntor  33072  lmod1  33093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-v 3111  df-sbc 3328  df-sn 4030
  Copyright terms: Public domain W3C validator