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

Definition df-ral 2717
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 2712 . 2
52cv 1653 . . . . 5
65, 3wcel 1728 . . . 4
76, 1wi 4 . . 3
87, 2wal 1550 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  ralnex  2722  rexnal  2723  ralbida  2726  ralbidv2  2734  ralbii2  2740  r2alf  2747  hbral  2761  hbra1  2762  nfra1  2763  nfrald  2764  r3al  2770  alral  2771  rsp  2773  rgen  2778  rgen2a  2779  ralim  2784  ralimi2  2785  ralimdaa  2790  ralimdv2  2793  ralrimi  2794  r19.21t  2798  ralrimd  2801  r19.21bi  2811  r19.23t  2827  r19.26m  2848  ralcom2  2879  rabid2  2892  rabbi  2893  raleqf  2907  cbvralf  2935  cbvraldva2  2945  ralv  2978  ceqsralt  2988  rspct  3054  rspc  3055  rspcimdv  3062  ralab  3104  ralab2  3108  ralrab2  3109  reu2  3131  reu6  3132  reu3  3133  rmo4  3136  reu8  3139  rmoim  3142  2reuswap  3145  2reu5lem2  3149  2reu5lem3  3150  ra5  3264  rmo2  3265  rmo3  3267  cbvralcsf  3300  dfss3  3327  dfss3f  3329  ssabral  3403  ss2rab  3408  rabss  3409  ssrab  3410  ralunb  3517  reuss2  3609  disj  3694  disj1  3696  r19.2z  3743  r19.3rz  3745  r19.3rzv  3747  ralidm  3757  ralf0  3760  ralsnsg  3871  unissb  4074  dfint2  4081  elint2  4086  elintrab  4091  ssintrab  4102  dfiin2g  4154  invdisj  4232  disjss3  4242  dftr5  4339  trint  4351  reusv2lem4  4768  find  4911  raliunxp  5056  dmopab3  5126  issref  5291  asymref  5294  asymref2  5295  dffun7  5526  funcnv  5558  funcnvuni  5565  fnres  5608  fnopabg  5615  dff3  5930  dffo3  5932  zfrep6  6016  tfrlem2  6686  nfixp  7130  marypha2lem3  7491  zfregcl  7611  zfinf2  7646  scottexs  7862  scott0s  7863  aceq1  8049  aceq2  8051  kmlem12  8092  kmlem14  8094  kmlem15  8095  zorn2lem4  8430  zorn2lem5  8431  ingru  8741  axgroth5  8750  grothprim  8760  sstskm  8768  supsrlem  9037  infm3  10018  nnunb  10268  nnwos  10595  fz1sbc  11175  caubnd  12213  rpnnen2  12876  isprm2  13138  pgpfac1  15689  pgpfac  15693  lidldvgen  16377  iunocv  16959  istopg  17019  bwth  17524  dfcon2  17533  1stccn  17577  iskgen3  17632  fbfinnfr  17924  iscmet3  19297  wilthlem3  20904  nbcusgra  21523  cusgrauvtxb  21556  isch3  22795  choc0  22879  pjnormssi  23722  rabid2f  24016  2reuswap2  24024  rmo3f  24031  rmo4fOLD  24032  ssiun3  24058  mptfnf  24121  fmcncfil  24366  untuni  25262  dfpo2  25482  dfon2lem8  25521  predreseq  25558  wzel  25679  dfrdg4  25899  onsuct0  26295  nninfnub  26566  mptbi12f  26863  n0el  26889  ralxpxfr2d  26922  dford4  27279  ralbidar  27803  rexbidar  27804  rexrsb  28101  2rmoswap  28116  ssralv2  28853  en3lpVD  29198  ssralv2VD  29219  trintALTVD  29233  bnj115  29331  bnj538  29349  bnj946  29386  bnj1142  29401  bnj1211  29410  bnj1294  29430  bnj1385  29445  bnj110  29470  bnj611  29530  bnj864  29534  bnj865  29535  bnj1000  29553  bnj978  29561  bnj1049  29584  bnj1090  29589  bnj1133  29599  bnj1176  29615  bnj1186  29617  bnj1253  29627  bnj1388  29643  pmapglbx  30806  cdlemefrs29bpre0  31433
  Copyright terms: Public domain W3C validator