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

Definition df-ral 2548
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 2543 . 2  wff  A. x  e.  A  ph
52cv 1622 . . . . 5  class  x
65, 3wcel 1684 . . . 4  wff  x  e.  A
76, 1wi 4 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1527 . 2  wff  A. x
( x  e.  A  ->  ph )
94, 8wb 176 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  2553  rexnal  2554  ralbida  2557  ralbidv2  2565  ralbii2  2571  r2alf  2578  hbral  2591  hbra1  2592  nfra1  2593  nfrald  2594  r3al  2600  alral  2601  rsp  2603  rgen  2608  rgen2a  2609  ralim  2614  ralimi2  2615  ralimdaa  2620  ralimdv2  2623  ralrimi  2624  r19.21t  2628  ralrimd  2631  r19.21bi  2641  r19.23t  2657  r19.26m  2678  ralcom2  2704  rabid2  2717  rabbi  2718  raleqf  2732  cbvralf  2758  cbvraldva2  2768  ralv  2801  ceqsralt  2811  rspct  2877  rspc  2878  rspcimdv  2885  ralab  2926  ralab2  2930  ralrab2  2931  reu2  2953  reu6  2954  reu3  2955  rmo4  2958  reu8  2961  rmoim  2964  2reuswap  2967  2reu5lem2  2971  2reu5lem3  2972  ra5  3075  rmo2  3076  rmo3  3078  cbvralcsf  3143  dfss3  3170  dfss3f  3172  ssabral  3244  ss2rab  3249  rabss  3250  ssrab  3251  ralunb  3356  reuss2  3448  disj  3495  disj1  3497  r19.2z  3543  r19.3rz  3545  r19.3rzv  3547  ralidm  3557  ralf0  3560  ralsns  3670  unissb  3857  dfint2  3864  elint2  3869  elintrab  3874  ssintrab  3885  dfiin2g  3936  invdisj  4012  disjss3  4022  dftr5  4116  trint  4128  reusv2lem4  4538  find  4681  raliunxp  4825  dmopab3  4891  issref  5056  asymref  5059  asymref2  5060  dffun7  5280  funcnv  5310  funcnvuni  5317  fnres  5360  fnopabg  5367  dff3  5673  dffo3  5675  zfrep6  5748  tfrlem2  6392  nfixp  6835  marypha2lem3  7190  zfregcl  7308  zfinf2  7343  scottexs  7557  scott0s  7558  aceq1  7744  aceq2  7746  kmlem12  7787  kmlem14  7789  kmlem15  7790  zorn2lem4  8126  zorn2lem5  8127  ingru  8437  axgroth5  8446  grothprim  8456  sstskm  8464  supsrlem  8733  infm3  9713  nnunb  9961  nnwos  10286  fz1sbc  10859  caubnd  11842  rpnnen2  12504  isprm2  12766  pgpfac1  15315  pgpfac  15319  lidldvgen  16007  iunocv  16581  istopg  16641  dfcon2  17145  1stccn  17189  iskgen3  17244  fbfinnfr  17536  iscmet3  18719  wilthlem3  20308  isch3  21821  choc0  21905  pjnormssi  22748  rabid2f  23135  2reuswap2  23137  ssiun3  23156  rmo3f  23178  rmo4fOLD  23179  mptfnf  23226  sigaclfu2  23482  untuni  24055  dfpo2  24112  dfon2lem8  24146  predreseq  24179  dfrdg4  24488  onsuct0  24880  fates  24955  domfldrefc  25057  ranfldrefc  25058  domrngref  25060  imfstnrelc  25081  qusp  25542  prcnt  25551  bwt2  25592  ismonc  25814  isepic  25824  isconcl7a  26105  nninfnub  26461  n0el  26725  ralxpxfr2d  26760  dford4  27122  ralbidar  27648  rexbidar  27649  stoweidlem52  27801  stoweidlem61  27810  rexrsb  27947  2rmoswap  27962  nbcusgra  28159  cusgrauvtx  28168  ssralv2  28294  en3lpVD  28621  ssralv2VD  28642  trintALTVD  28656  bnj115  28751  bnj538  28769  bnj946  28806  bnj1142  28821  bnj1211  28830  bnj1294  28850  bnj1385  28865  bnj110  28890  bnj611  28950  bnj864  28954  bnj865  28955  bnj1000  28973  bnj978  28981  bnj1049  29004  bnj1090  29009  bnj1133  29019  bnj1176  29035  bnj1186  29037  bnj1253  29047  bnj1388  29063  pmapglbx  29958  cdlemefrs29bpre0  30585
  Copyright terms: Public domain W3C validator