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

Definition df-ral 2671
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 2666 . 2  wff  A. x  e.  A  ph
52cv 1648 . . . . 5  class  x
65, 3wcel 1721 . . . 4  wff  x  e.  A
76, 1wi 4 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1546 . 2  wff  A. x
( x  e.  A  ->  ph )
94, 8wb 177 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  2676  rexnal  2677  ralbida  2680  ralbidv2  2688  ralbii2  2694  r2alf  2701  hbral  2714  hbra1  2715  nfra1  2716  nfrald  2717  r3al  2723  alral  2724  rsp  2726  rgen  2731  rgen2a  2732  ralim  2737  ralimi2  2738  ralimdaa  2743  ralimdv2  2746  ralrimi  2747  r19.21t  2751  ralrimd  2754  r19.21bi  2764  r19.23t  2780  r19.26m  2801  ralcom2  2832  rabid2  2845  rabbi  2846  raleqf  2860  cbvralf  2886  cbvraldva2  2896  ralv  2929  ceqsralt  2939  rspct  3005  rspc  3006  rspcimdv  3013  ralab  3055  ralab2  3059  ralrab2  3060  reu2  3082  reu6  3083  reu3  3084  rmo4  3087  reu8  3090  rmoim  3093  2reuswap  3096  2reu5lem2  3100  2reu5lem3  3101  ra5  3205  rmo2  3206  rmo3  3208  cbvralcsf  3271  dfss3  3298  dfss3f  3300  ssabral  3374  ss2rab  3379  rabss  3380  ssrab  3381  ralunb  3488  reuss2  3581  disj  3628  disj1  3630  r19.2z  3677  r19.3rz  3679  r19.3rzv  3681  ralidm  3691  ralf0  3694  ralsns  3804  unissb  4005  dfint2  4012  elint2  4017  elintrab  4022  ssintrab  4033  dfiin2g  4084  invdisj  4161  disjss3  4171  dftr5  4265  trint  4277  reusv2lem4  4686  find  4829  raliunxp  4973  dmopab3  5041  issref  5206  asymref  5209  asymref2  5210  dffun7  5438  funcnv  5470  funcnvuni  5477  fnres  5520  fnopabg  5527  dff3  5841  dffo3  5843  zfrep6  5927  tfrlem2  6596  nfixp  7040  marypha2lem3  7400  zfregcl  7518  zfinf2  7553  scottexs  7767  scott0s  7768  aceq1  7954  aceq2  7956  kmlem12  7997  kmlem14  7999  kmlem15  8000  zorn2lem4  8335  zorn2lem5  8336  ingru  8646  axgroth5  8655  grothprim  8665  sstskm  8673  supsrlem  8942  infm3  9923  nnunb  10173  nnwos  10500  fz1sbc  11079  caubnd  12117  rpnnen2  12780  isprm2  13042  pgpfac1  15593  pgpfac  15597  lidldvgen  16281  iunocv  16863  istopg  16923  dfcon2  17435  1stccn  17479  iskgen3  17534  fbfinnfr  17826  iscmet3  19199  wilthlem3  20806  nbcusgra  21425  cusgrauvtxb  21458  isch3  22697  choc0  22781  pjnormssi  23624  rabid2f  23920  2reuswap2  23928  rmo3f  23935  rmo4fOLD  23936  ssiun3  23962  mptfnf  24026  fmcncfil  24270  untuni  25111  dfpo2  25326  dfon2lem8  25360  predreseq  25393  dfrdg4  25703  onsuct0  26095  nninfnub  26345  n0el  26598  ralxpxfr2d  26631  dford4  26990  ralbidar  27515  rexbidar  27516  rexrsb  27814  2rmoswap  27829  ssralv2  28326  en3lpVD  28666  ssralv2VD  28687  trintALTVD  28701  bnj115  28796  bnj538  28814  bnj946  28851  bnj1142  28866  bnj1211  28875  bnj1294  28895  bnj1385  28910  bnj110  28935  bnj611  28995  bnj864  28999  bnj865  29000  bnj1000  29018  bnj978  29026  bnj1049  29049  bnj1090  29054  bnj1133  29064  bnj1176  29080  bnj1186  29082  bnj1253  29092  bnj1388  29108  pmapglbx  30251  cdlemefrs29bpre0  30878
  Copyright terms: Public domain W3C validator