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

Definition df-ral 2812
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 2807 . 2
52cv 1394 . . . . 5
65, 3wcel 1818 . . . 4
76, 1wi 4 . . 3
87, 2wal 1393 . 2
94, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  rgen  2817  alral  2822  rsp  2823  r19.21biOLD  2827  r2allem  2832  r2alfOLD  2834  r3al  2837  nfra1  2838  hbra1OLD  2840  hbral  2841  nfrald  2842  ral2imi  2845  ralimi2  2847  ralimOLD  2851  hbralrimi  2853  r19.21t  2854  r19.21tOLD  2855  ralrimiOLD  2858  ralimdaaOLD  2860  ralrimd  2861  r19.21v  2862  ralimdv2  2864  rgen2a  2884  rgen2aOLD  2885  ralbii2  2886  ralbida  2890  ralbidv2  2892  r3alOLD  2895  ralnex  2903  rexnalOLD  2906  r19.23t  2935  r19.26m  2987  ralcom2  3022  rabid2  3035  rabbi  3036  raleqf  3050  cbvralf  3078  cbvraldva2  3088  ralv  3123  ceqsralt  3133  rspct  3203  rspc  3204  rspcimdv  3211  ralxpxfr2d  3224  ralab  3260  ralab2  3264  ralrab2  3265  reu2  3287  reu6  3288  reu3  3289  rmo4  3292  reu8  3295  rmoim  3299  2reuswap  3302  2reu5lem2  3306  2reu5lem3  3307  ra4vOLD  3424  ra4OLD  3426  rmo2  3427  rmo3  3429  cbvralcsf  3466  dfss3  3493  dfss3f  3495  ssabral  3570  ss2rab  3575  rabss  3576  ssrab  3577  ralunb  3684  reuss2  3777  disj  3867  disj1  3869  r19.2z  3918  r19.3rz  3920  r19.3rzv  3922  ralidm  3933  ralf0  3936  ralsnsg  4061  unissb  4281  dfint2  4288  elint2  4293  elintrab  4298  ssintrab  4310  dfiin2g  4363  invdisj  4441  disjss3  4451  dftr5  4548  trint  4560  reusv2lem4  4656  raliunxp  5147  dmopab3  5220  issref  5385  asymref  5388  asymref2  5389  dffun7  5619  funcnv  5653  fnres  5702  fnopabg  5709  dff3  6044  dffo3  6046  find  6725  funcnvuni  6753  zfrep6  6768  nfixp  7508  marypha2lem3  7917  zfregcl  8041  zfinf2  8080  scottexs  8326  scott0s  8327  aceq1  8519  aceq2  8521  kmlem12  8562  kmlem14  8564  kmlem15  8565  zorn2lem4  8900  zorn2lem5  8901  ingru  9214  axgroth5  9223  grothprim  9233  sstskm  9241  supsrlem  9509  infm3  10527  nnunb  10816  nnwos  11178  fz1sbc  11783  caubnd  13191  rpnnen2  13959  isprm2  14225  pgpfac1  17131  pgpfac  17135  lidldvgen  17903  iunocv  18712  istopg  19404  bwthOLD  19911  dfcon2  19920  1stccn  19964  iskgen3  20050  fbfinnfr  20342  iscmet3  21732  wilthlem3  23344  nbcusgra  24463  cusgrauvtxb  24496  isch3  26159  choc0  26244  pjnormssi  27087  moel  27382  2reuswap2  27387  rmo3f  27394  rmo4fOLD  27395  rabid2f  27400  ssiun3  27426  mptfnf  27499  fmcncfil  27913  untuni  29081  dfpo2  29184  dfon2lem8  29222  predreseq  29259  wzel  29380  dfrdg4  29600  onsuct0  29906  nninfnub  30244  mptbi12f  30575  n0el  30600  dford4  30971  ralbidar  31354  rexbidar  31355  rexrsb  32174  2rmoswap  32189  nrhmzr  32679  rabsssn  32920  empty-surprise  33197  alsconv  33205  ssralv2  33301  en3lpVD  33645  ssralv2VD  33666  trintALTVD  33680  bnj115  33778  bnj538OLD  33797  bnj946  33833  bnj1142  33848  bnj1211  33856  bnj1294  33876  bnj1385  33891  bnj110  33916  bnj611  33976  bnj864  33980  bnj865  33981  bnj1000  33999  bnj978  34007  bnj1049  34030  bnj1090  34035  bnj1133  34045  bnj1176  34061  bnj1186  34063  bnj1253  34073  bnj1388  34089  bj-ralvw  34441  bj-ralcom4  34444  pmapglbx  35493  cdlemefrs29bpre0  36122  cllem0  37751  elintima  37765  cotr2g  37786
  Copyright terms: Public domain W3C validator