MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ral Structured version   Unicode version

Definition df-ral 2710
Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
Assertion
Ref Expression
df-ral  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )

Detailed syntax breakdown of Definition df-ral
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  set  x
3 cA . . 3  class  A
41, 2, 3wral 2705 . 2  wff  A. x  e.  A  ph
52cv 1651 . . . . 5  class  x
65, 3wcel 1725 . . . 4  wff  x  e.  A
76, 1wi 4 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1549 . 2  wff  A. x
( x  e.  A  ->  ph )
94, 8wb 177 1  wff  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
Colors of variables: wff set class
This definition is referenced by:  ralnex  2715  rexnal  2716  ralbida  2719  ralbidv2  2727  ralbii2  2733  r2alf  2740  hbral  2754  hbra1  2755  nfra1  2756  nfrald  2757  r3al  2763  alral  2764  rsp  2766  rgen  2771  rgen2a  2772  ralim  2777  ralimi2  2778  ralimdaa  2783  ralimdv2  2786  ralrimi  2787  r19.21t  2791  ralrimd  2794  r19.21bi  2804  r19.23t  2820  r19.26m  2841  ralcom2  2872  rabid2  2885  rabbi  2886  raleqf  2900  cbvralf  2926  cbvraldva2  2936  ralv  2969  ceqsralt  2979  rspct  3045  rspc  3046  rspcimdv  3053  ralab  3095  ralab2  3099  ralrab2  3100  reu2  3122  reu6  3123  reu3  3124  rmo4  3127  reu8  3130  rmoim  3133  2reuswap  3136  2reu5lem2  3140  2reu5lem3  3141  ra5  3245  rmo2  3246  rmo3  3248  cbvralcsf  3311  dfss3  3338  dfss3f  3340  ssabral  3414  ss2rab  3419  rabss  3420  ssrab  3421  ralunb  3528  reuss2  3621  disj  3668  disj1  3670  r19.2z  3717  r19.3rz  3719  r19.3rzv  3721  ralidm  3731  ralf0  3734  ralsns  3844  unissb  4045  dfint2  4052  elint2  4057  elintrab  4062  ssintrab  4073  dfiin2g  4124  invdisj  4201  disjss3  4211  dftr5  4305  trint  4317  reusv2lem4  4727  find  4870  raliunxp  5014  dmopab3  5082  issref  5247  asymref  5250  asymref2  5251  dffun7  5479  funcnv  5511  funcnvuni  5518  fnres  5561  fnopabg  5568  dff3  5882  dffo3  5884  zfrep6  5968  tfrlem2  6637  nfixp  7081  marypha2lem3  7442  zfregcl  7562  zfinf2  7597  scottexs  7811  scott0s  7812  aceq1  7998  aceq2  8000  kmlem12  8041  kmlem14  8043  kmlem15  8044  zorn2lem4  8379  zorn2lem5  8380  ingru  8690  axgroth5  8699  grothprim  8709  sstskm  8717  supsrlem  8986  infm3  9967  nnunb  10217  nnwos  10544  fz1sbc  11124  caubnd  12162  rpnnen2  12825  isprm2  13087  pgpfac1  15638  pgpfac  15642  lidldvgen  16326  iunocv  16908  istopg  16968  bwth  17473  dfcon2  17482  1stccn  17526  iskgen3  17581  fbfinnfr  17873  iscmet3  19246  wilthlem3  20853  nbcusgra  21472  cusgrauvtxb  21505  isch3  22744  choc0  22828  pjnormssi  23671  rabid2f  23967  2reuswap2  23975  rmo3f  23982  rmo4fOLD  23983  ssiun3  24009  mptfnf  24073  fmcncfil  24317  untuni  25158  dfpo2  25378  dfon2lem8  25417  predreseq  25454  wzel  25575  dfrdg4  25795  onsuct0  26191  nninfnub  26455  n0el  26708  ralxpxfr2d  26741  dford4  27100  ralbidar  27624  rexbidar  27625  rexrsb  27923  2rmoswap  27938  ssralv2  28615  en3lpVD  28957  ssralv2VD  28978  trintALTVD  28992  bnj115  29090  bnj538  29108  bnj946  29145  bnj1142  29160  bnj1211  29169  bnj1294  29189  bnj1385  29204  bnj110  29229  bnj611  29289  bnj864  29293  bnj865  29294  bnj1000  29312  bnj978  29320  bnj1049  29343  bnj1090  29348  bnj1133  29358  bnj1176  29374  bnj1186  29376  bnj1253  29386  bnj1388  29402  pmapglbx  30566  cdlemefrs29bpre0  31193
  Copyright terms: Public domain W3C validator