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

Definition df-ral 2520
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  2524  rexnal  2525  ralbida  2528  ralbidv2  2536  ralbii2  2542  r2alf  2549  hbral  2562  hbra1  2563  nfra1  2564  nfrald  2565  r3al  2571  alral  2572  ra4  2574  rgen  2579  rgen2a  2580  ralim  2585  ralimi2  2586  ralimdaa  2591  ralimdv2  2594  ralrimi  2595  r19.21t  2599  ralrimd  2602  r19.21bi  2612  r19.23t  2628  r19.26m  2649  ralcom2  2675  rabid2  2685  rabbi  2686  raleqf  2695  cbvralf  2712  cbvraldva2  2720  ralv  2753  ceqsralt  2762  rcla4t  2828  rcla4  2829  rcla4imdv  2836  ralab  2877  ralab2  2881  ralrab2  2882  reu2  2906  reu6  2907  reu3  2908  rmo4  2911  reu8  2914  2reuswap  2916  ra5  3019  rmo3  3020  cbvralcsf  3085  dfss3  3112  dfss3f  3114  ssabral  3186  ss2rab  3191  rabss  3192  ssrab  3193  ralunb  3298  reuss2  3390  disj  3437  disj1  3439  r19.2z  3485  r19.3rz  3487  r19.3rzv  3489  ralidm  3499  ralf0  3502  ralsns  3611  unissb  3798  dfint2  3805  elint2  3810  elintrab  3815  ssintrab  3826  dfiin2g  3877  disjss2  3936  invdisj  3952  disjiun  3953  disjss3  3962  dftr5  4056  trint  4068  reusv2lem4  4475  find  4618  raliunxp  4778  dmopab3  4844  issref  5009  asymref  5012  asymref2  5013  dffun7  5184  funcnv  5213  funcnvuni  5220  fnres  5263  fnopabg  5270  dff3  5572  dffo3  5574  zfrep6  5647  tfrlem2  6325  nfixp  6768  marypha2lem3  7123  zfregcl  7241  zfinf2  7276  scottexs  7490  scott0s  7491  aceq1  7677  aceq2  7679  kmlem12  7720  kmlem14  7722  kmlem15  7723  zorn2lem4  8059  zorn2lem5  8060  ingru  8370  axgroth5  8379  grothprim  8389  sstskm  8397  supsrlem  8666  infm3  9646  nnunb  9893  nnwos  10218  fz1sbc  10790  caubnd  11772  rpnnen2  12431  isprm2  12693  pgpfac1  15242  pgpfac  15246  lidldvgen  15934  iunocv  16508  istopg  16568  dfcon2  17072  2ndcdisj  17109  1stccn  17116  iskgen3  17171  fbfinnfr  17463  iscmet3  18646  wilthlem3  20235  isch3  21746  choc0  21830  pjnormssi  22673  untuni  23392  dfpo2  23448  dfon2lem8  23480  predreseq  23513  dfrdg4  23828  onsuct0  24220  fates  24286  domfldrefc  24388  ranfldrefc  24389  domrngref  24391  imfstnrelc  24412  qusp  24874  prcnt  24883  bwt2  24924  ismonc  25146  isepic  25156  isconcl7a  25437  nninfnub  25793  n0el  26057  ralxpxfr2d  26092  dford4  26454  ralbidar  26981  rexbidar  26982  stoweidlem52  27101  stoweidlem61  27110  ssralv2  27310  en3lpVD  27634  ssralv2VD  27655  trintALTVD  27669  bnj115  27763  bnj538  27781  bnj946  27818  bnj1142  27833  bnj1211  27842  bnj1294  27862  bnj1385  27877  bnj110  27902  bnj611  27962  bnj864  27966  bnj865  27967  bnj1000  27985  bnj978  27993  bnj1049  28016  bnj1090  28021  bnj1133  28031  bnj1176  28047  bnj1186  28049  bnj1253  28059  bnj1388  28075  pmapglbx  29088  cdlemefrs29bpre0  29715
  Copyright terms: Public domain W3C validator