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

Definition df-ral 2513
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 2509 . 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  2517  rexnal  2518  ralbida  2521  ralbidv2  2529  ralbii2  2535  r2alf  2540  hbral  2553  hbra1  2554  nfra1  2555  nfrald  2556  r3al  2562  alral  2563  ra4  2565  rgen  2570  rgen2a  2571  ralim  2576  ralimi2  2577  ralimdaa  2582  ralimdv2  2585  ralrimi  2586  r19.21t  2590  ralrimd  2593  r19.21bi  2603  r19.23t  2619  r19.26m  2640  ralcom2  2666  rabid2  2676  rabbi  2677  raleqf  2686  cbvralf  2703  ralv  2740  ceqsralt  2749  rcla4t  2814  rcla4  2815  rcla4imdv  2822  ralab  2863  ralab2  2867  ralrab2  2868  reu2  2892  reu6  2893  reu3  2894  rmo4  2897  reu8  2900  2reuswap  2902  ra5  3005  rmo3  3006  cbvralcsf  3071  dfss3  3093  dfss3f  3095  ssabral  3165  ss2rab  3170  rabss  3171  ssrab  3172  ralunb  3264  reuss2  3355  disj  3402  disj1  3404  r19.2z  3449  r19.3rz  3451  r19.3rzv  3453  ralidm  3463  ralf0  3466  ralsns  3574  unissb  3755  dfint2  3762  elint2  3767  elintrab  3772  ssintrab  3783  dfiin2g  3834  disjss2  3893  invdisj  3909  disjiun  3910  disjss3  3919  dftr5  4013  trint  4025  reusv2lem4  4429  find  4572  raliunxp  4732  dmopab3  4798  issref  4963  asymref  4966  asymref2  4967  dffun7  5138  funcnv  5167  funcnvuni  5174  fnres  5217  fnopabg  5224  dff3  5525  dffo3  5527  zfrep6  5600  tfrlem2  6278  nfixp  6721  marypha2lem3  7074  zfregcl  7192  zfinf2  7227  scottexs  7441  scott0s  7442  aceq1  7628  aceq2  7630  kmlem12  7671  kmlem14  7673  kmlem15  7674  zorn2lem4  8010  zorn2lem5  8011  ingru  8317  axgroth5  8326  grothprim  8336  sstskm  8344  supsrlem  8613  infm3  9593  nnunb  9840  nnwos  10165  fz1sbc  10737  caubnd  11719  rpnnen2  12378  isprm2  12640  pgpfac1  15150  pgpfac  15154  lidldvgen  15839  iunocv  16413  istopg  16473  dfcon2  16977  2ndcdisj  17014  1stccn  17021  iskgen3  17076  fbfinnfr  17368  iscmet3  18551  wilthlem3  20140  isch3  21651  choc0  21735  pjnormssi  22578  untuni  23226  dfpo2  23282  dfon2lem8  23314  predreseq  23347  dfrdg4  23662  onsuct0  24054  fates  24120  domfldrefc  24222  ranfldrefc  24223  domrngref  24225  imfstnrelc  24246  qusp  24708  prcnt  24717  bwt2  24758  ismonc  24980  isepic  24990  isconcl7a  25271  nninfnub  25627  n0el  25891  ralxpxfr2d  25926  dford4  26288  ralbidar  26815  rexbidar  26816  ssralv2  26987  en3lpVD  27311  ssralv2VD  27332  trintALTVD  27346  bnj115  27440  bnj538  27458  bnj946  27495  bnj1142  27510  bnj1211  27519  bnj1294  27539  bnj1385  27554  bnj110  27579  bnj611  27639  bnj864  27643  bnj865  27644  bnj1000  27662  bnj978  27670  bnj1049  27693  bnj1090  27698  bnj1133  27708  bnj1176  27724  bnj1186  27726  bnj1253  27736  bnj1388  27752  pmapglbx  28759  cdlemefrs29bpre0  29386
  Copyright terms: Public domain W3C validator