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

Definition df-ral 2521
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 2516 . 2  wff  A. x  e.  A  ph
52cv 1618 . . . . 5  class  x
65, 3wcel 1621 . . . 4  wff  x  e.  A
76, 1wi 6 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1532 . 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  2526  rexnal  2527  ralbida  2530  ralbidv2  2538  ralbii2  2544  r2alf  2551  hbral  2564  hbra1  2565  nfra1  2566  nfrald  2567  r3al  2573  alral  2574  ra4  2576  rgen  2581  rgen2a  2582  ralim  2587  ralimi2  2588  ralimdaa  2593  ralimdv2  2596  ralrimi  2597  r19.21t  2601  ralrimd  2604  r19.21bi  2614  r19.23t  2630  r19.26m  2651  ralcom2  2677  rabid2  2690  rabbi  2691  raleqf  2705  cbvralf  2728  cbvraldva2  2737  ralv  2770  ceqsralt  2779  rcla4t  2845  rcla4  2846  rcla4imdv  2853  ralab  2894  ralab2  2898  ralrab2  2899  reu2  2921  reu6  2922  reu3  2923  rmo4  2926  reu8  2929  imrmo  2932  2reuswap  2933  ra5  3036  rmo2  3037  rmo3  3039  cbvralcsf  3104  dfss3  3131  dfss3f  3133  ssabral  3205  ss2rab  3210  rabss  3211  ssrab  3212  ralunb  3317  reuss2  3409  disj  3456  disj1  3458  r19.2z  3504  r19.3rz  3506  r19.3rzv  3508  ralidm  3518  ralf0  3521  ralsns  3630  unissb  3817  dfint2  3824  elint2  3829  elintrab  3834  ssintrab  3845  dfiin2g  3896  invdisj  3972  disjss3  3982  dftr5  4076  trint  4088  reusv2lem4  4496  find  4639  raliunxp  4799  dmopab3  4865  issref  5030  asymref  5033  asymref2  5034  dffun7  5205  funcnv  5234  funcnvuni  5241  fnres  5284  fnopabg  5291  dff3  5593  dffo3  5595  zfrep6  5668  tfrlem2  6346  nfixp  6789  marypha2lem3  7144  zfregcl  7262  zfinf2  7297  scottexs  7511  scott0s  7512  aceq1  7698  aceq2  7700  kmlem12  7741  kmlem14  7743  kmlem15  7744  zorn2lem4  8080  zorn2lem5  8081  ingru  8391  axgroth5  8400  grothprim  8410  sstskm  8418  supsrlem  8687  infm3  9667  nnunb  9914  nnwos  10239  fz1sbc  10811  caubnd  11793  rpnnen2  12452  isprm2  12714  pgpfac1  15263  pgpfac  15267  lidldvgen  15955  iunocv  16529  istopg  16589  dfcon2  17093  1stccn  17137  iskgen3  17192  fbfinnfr  17484  iscmet3  18667  wilthlem3  20256  isch3  21767  choc0  21851  pjnormssi  22694  untuni  23413  dfpo2  23469  dfon2lem8  23501  predreseq  23534  dfrdg4  23849  onsuct0  24241  fates  24307  domfldrefc  24409  ranfldrefc  24410  domrngref  24412  imfstnrelc  24433  qusp  24895  prcnt  24904  bwt2  24945  ismonc  25167  isepic  25177  isconcl7a  25458  nninfnub  25814  n0el  26078  ralxpxfr2d  26113  dford4  26475  ralbidar  27002  rexbidar  27003  stoweidlem52  27122  stoweidlem61  27131  ssralv2  27331  en3lpVD  27655  ssralv2VD  27676  trintALTVD  27690  bnj115  27784  bnj538  27802  bnj946  27839  bnj1142  27854  bnj1211  27863  bnj1294  27883  bnj1385  27898  bnj110  27923  bnj611  27983  bnj864  27987  bnj865  27988  bnj1000  28006  bnj978  28014  bnj1049  28037  bnj1090  28042  bnj1133  28052  bnj1176  28068  bnj1186  28070  bnj1253  28080  bnj1388  28096  pmapglbx  29109  cdlemefrs29bpre0  29736
  Copyright terms: Public domain W3C validator