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

Definition df-ral 2712
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 2707 . 2  wff  A. x  e.  A  ph
52cv 1652 . . . . 5  class  x
65, 3wcel 1726 . . . 4  wff  x  e.  A
76, 1wi 4 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1550 . 2  wff  A. x
( x  e.  A  ->  ph )
94, 8wb 178 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  2717  rexnal  2718  ralbida  2721  ralbidv2  2729  ralbii2  2735  r2alf  2742  hbral  2756  hbra1  2757  nfra1  2758  nfrald  2759  r3al  2765  alral  2766  rsp  2768  rgen  2773  rgen2a  2774  ralim  2779  ralimi2  2780  ralimdaa  2785  ralimdv2  2788  ralrimi  2789  r19.21t  2793  ralrimd  2796  r19.21bi  2806  r19.23t  2822  r19.26m  2843  ralcom2  2874  rabid2  2887  rabbi  2888  raleqf  2902  cbvralf  2928  cbvraldva2  2938  ralv  2971  ceqsralt  2981  rspct  3047  rspc  3048  rspcimdv  3055  ralab  3097  ralab2  3101  ralrab2  3102  reu2  3124  reu6  3125  reu3  3126  rmo4  3129  reu8  3132  rmoim  3135  2reuswap  3138  2reu5lem2  3142  2reu5lem3  3143  ra5  3247  rmo2  3248  rmo3  3250  cbvralcsf  3313  dfss3  3340  dfss3f  3342  ssabral  3416  ss2rab  3421  rabss  3422  ssrab  3423  ralunb  3530  reuss2  3623  disj  3670  disj1  3672  r19.2z  3719  r19.3rz  3721  r19.3rzv  3723  ralidm  3733  ralf0  3736  ralsns  3846  unissb  4047  dfint2  4054  elint2  4059  elintrab  4064  ssintrab  4075  dfiin2g  4126  invdisj  4204  disjss3  4214  dftr5  4308  trint  4320  reusv2lem4  4730  find  4873  raliunxp  5017  dmopab3  5085  issref  5250  asymref  5253  asymref2  5254  dffun7  5482  funcnv  5514  funcnvuni  5521  fnres  5564  fnopabg  5571  dff3  5885  dffo3  5887  zfrep6  5971  tfrlem2  6640  nfixp  7084  marypha2lem3  7445  zfregcl  7565  zfinf2  7600  scottexs  7816  scott0s  7817  aceq1  8003  aceq2  8005  kmlem12  8046  kmlem14  8048  kmlem15  8049  zorn2lem4  8384  zorn2lem5  8385  ingru  8695  axgroth5  8704  grothprim  8714  sstskm  8722  supsrlem  8991  infm3  9972  nnunb  10222  nnwos  10549  fz1sbc  11129  caubnd  12167  rpnnen2  12830  isprm2  13092  pgpfac1  15643  pgpfac  15647  lidldvgen  16331  iunocv  16913  istopg  16973  bwth  17478  dfcon2  17487  1stccn  17531  iskgen3  17586  fbfinnfr  17878  iscmet3  19251  wilthlem3  20858  nbcusgra  21477  cusgrauvtxb  21510  isch3  22749  choc0  22833  pjnormssi  23676  rabid2f  23972  2reuswap2  23980  rmo3f  23987  rmo4fOLD  23988  ssiun3  24014  mptfnf  24078  fmcncfil  24322  untuni  25163  dfpo2  25383  dfon2lem8  25422  predreseq  25459  wzel  25580  dfrdg4  25800  onsuct0  26196  nninfnub  26469  n0el  26722  ralxpxfr2d  26755  dford4  27114  ralbidar  27638  rexbidar  27639  rexrsb  27937  2rmoswap  27952  ssralv2  28689  en3lpVD  29031  ssralv2VD  29052  trintALTVD  29066  bnj115  29164  bnj538  29182  bnj946  29219  bnj1142  29234  bnj1211  29243  bnj1294  29263  bnj1385  29278  bnj110  29303  bnj611  29363  bnj864  29367  bnj865  29368  bnj1000  29386  bnj978  29394  bnj1049  29417  bnj1090  29422  bnj1133  29432  bnj1176  29448  bnj1186  29450  bnj1253  29460  bnj1388  29476  pmapglbx  30640  cdlemefrs29bpre0  31267
  Copyright terms: Public domain W3C validator