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

Definition df-ral 2764
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

Detailed syntax breakdown of Definition df-ral
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 cA . . 3
41, 2, 3wral 2759 . 2
52cv 1669 . . . . 5
65, 3wcel 1732 . . . 4
76, 1wi 4 . . 3
87, 2wal 1564 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  ralnex  2769  rexnal  2770  ralbida  2773  ralbidv2  2781  ralbii2  2787  r2alf  2794  hbral  2808  hbra1  2809  nfra1  2810  nfrald  2811  r3al  2817  alral  2818  rsp  2820  rgen  2825  rgen2a  2826  ralim  2831  ralimi2  2832  ralimdaa  2837  ralimdv2  2840  ralrimi  2841  r19.21t  2845  ralrimd  2848  r19.21bi  2858  r19.23t  2874  r19.26m  2895  ralcom2  2928  rabid2  2941  rabbi  2942  raleqf  2956  cbvralf  2984  cbvraldva2  2994  ralv  3028  ceqsralt  3038  rspct  3106  rspc  3107  rspcimdv  3114  ralab  3158  ralab2  3162  ralrab2  3163  reu2  3185  reu6  3186  reu3  3187  rmo4  3190  reu8  3193  rmoim  3196  2reuswap  3199  2reu5lem2  3203  2reu5lem3  3204  ra4  3319  rmo2  3320  rmo3  3322  cbvralcsf  3356  dfss3  3383  dfss3f  3385  ssabral  3460  ss2rab  3465  rabss  3466  ssrab  3467  ralunb  3574  reuss2  3666  disj  3754  disj1  3756  r19.2z  3803  r19.3rz  3805  r19.3rzv  3807  ralidm  3817  ralf0  3820  ralsnsg  3941  unissb  4149  dfint2  4156  elint2  4161  elintrab  4166  ssintrab  4177  dfiin2g  4229  invdisj  4307  disjss3  4317  dftr5  4414  trint  4426  reusv2lem4  4519  raliunxp  5001  dmopab3  5074  issref  5234  asymref  5237  asymref2  5238  dffun7  5464  funcnv  5496  fnres  5545  fnopabg  5552  dff3  5872  dffo3  5874  find  6511  funcnvuni  6537  zfrep6  6552  tfrlem2  6799  nfixp  7245  marypha2lem3  7609  zfregcl  7729  zfinf2  7764  scottexs  7980  scott0s  7981  aceq1  8169  aceq2  8171  kmlem12  8212  kmlem14  8214  kmlem15  8215  zorn2lem4  8550  zorn2lem5  8551  ingru  8861  axgroth5  8870  grothprim  8880  sstskm  8888  supsrlem  9157  infm3  10155  nnunb  10441  nnwos  10786  fz1sbc  11388  caubnd  12693  rpnnen2  13355  isprm2  13618  pgpfac1  16253  pgpfac  16257  lidldvgen  16951  iunocv  17533  istopg  17982  bwthOLD  18488  dfcon2  18497  1stccn  18541  iskgen3  18596  fbfinnfr  18888  iscmet3  20261  wilthlem3  21874  nbcusgra  22493  cusgrauvtxb  22526  isch3  23766  choc0  23851  pjnormssi  24694  moel  24995  2reuswap2  25000  rmo3f  25007  rmo4fOLD  25008  rabid2f  25013  ssiun3  25037  mptfnf  25106  fmcncfil  25540  untuni  26500  dfpo2  26717  dfon2lem8  26756  predreseq  26793  wzel  26914  dfrdg4  27134  onsuct0  27530  nninfnub  27827  mptbi12f  28122  n0el  28148  ralxpxfr2d  28175  dford4  28526  ralbidar  28875  rexbidar  28876  rexrsb  29172  2rmoswap  29187  empty-surprise  29986  alsconv  29994  ssralv2  30082  en3lpVD  30427  ssralv2VD  30448  trintALTVD  30462  bnj115  30560  bnj538  30578  bnj946  30615  bnj1142  30630  bnj1211  30639  bnj1294  30659  bnj1385  30674  bnj110  30699  bnj611  30759  bnj864  30763  bnj865  30764  bnj1000  30782  bnj978  30790  bnj1049  30813  bnj1090  30818  bnj1133  30828  bnj1176  30844  bnj1186  30846  bnj1253  30856  bnj1388  30872  pmapglbx  32116  cdlemefrs29bpre0  32743
  Copyright terms: Public domain W3C validator