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  untuni  23466  dfpo2  23523  dfon2lem8  23557  predreseq  23590  dfrdg4  23899  onsuct0  24291  fates  24367  domfldrefc  24469  ranfldrefc  24470  domrngref  24472  imfstnrelc  24493  qusp  24954  prcnt  24963  bwt2  25004  ismonc  25226  isepic  25236  isconcl7a  25517  nninfnub  25873  n0el  26137  ralxpxfr2d  26172  dford4  26534  ralbidar  27060  rexbidar  27061  stoweidlem52  27213  stoweidlem61  27222  rexrsb  27359  2rmoswap  27374  ssralv2  27667  en3lpVD  27994  ssralv2VD  28015  trintALTVD  28029  bnj115  28124  bnj538  28142  bnj946  28179  bnj1142  28194  bnj1211  28203  bnj1294  28223  bnj1385  28238  bnj110  28263  bnj611  28323  bnj864  28327  bnj865  28328  bnj1000  28346  bnj978  28354  bnj1049  28377  bnj1090  28382  bnj1133  28392  bnj1176  28408  bnj1186  28410  bnj1253  28420  bnj1388  28436  pmapglbx  29331  cdlemefrs29bpre0  29958
  Copyright terms: Public domain W3C validator