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

Definition df-ral 2561
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 2556 . 2  wff  A. x  e.  A  ph
52cv 1631 . . . . 5  class  x
65, 3wcel 1696 . . . 4  wff  x  e.  A
76, 1wi 4 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1530 . 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  2566  rexnal  2567  ralbida  2570  ralbidv2  2578  ralbii2  2584  r2alf  2591  hbral  2604  hbra1  2605  nfra1  2606  nfrald  2607  r3al  2613  alral  2614  rsp  2616  rgen  2621  rgen2a  2622  ralim  2627  ralimi2  2628  ralimdaa  2633  ralimdv2  2636  ralrimi  2637  r19.21t  2641  ralrimd  2644  r19.21bi  2654  r19.23t  2670  r19.26m  2691  ralcom2  2717  rabid2  2730  rabbi  2731  raleqf  2745  cbvralf  2771  cbvraldva2  2781  ralv  2814  ceqsralt  2824  rspct  2890  rspc  2891  rspcimdv  2898  ralab  2939  ralab2  2943  ralrab2  2944  reu2  2966  reu6  2967  reu3  2968  rmo4  2971  reu8  2974  rmoim  2977  2reuswap  2980  2reu5lem2  2984  2reu5lem3  2985  ra5  3088  rmo2  3089  rmo3  3091  cbvralcsf  3156  dfss3  3183  dfss3f  3185  ssabral  3257  ss2rab  3262  rabss  3263  ssrab  3264  ralunb  3369  reuss2  3461  disj  3508  disj1  3510  r19.2z  3556  r19.3rz  3558  r19.3rzv  3560  ralidm  3570  ralf0  3573  ralsns  3683  unissb  3873  dfint2  3880  elint2  3885  elintrab  3890  ssintrab  3901  dfiin2g  3952  invdisj  4028  disjss3  4038  dftr5  4132  trint  4144  reusv2lem4  4554  find  4697  raliunxp  4841  dmopab3  4907  issref  5072  asymref  5075  asymref2  5076  dffun7  5296  funcnv  5326  funcnvuni  5333  fnres  5376  fnopabg  5383  dff3  5689  dffo3  5691  zfrep6  5764  tfrlem2  6408  nfixp  6851  marypha2lem3  7206  zfregcl  7324  zfinf2  7359  scottexs  7573  scott0s  7574  aceq1  7760  aceq2  7762  kmlem12  7803  kmlem14  7805  kmlem15  7806  zorn2lem4  8142  zorn2lem5  8143  ingru  8453  axgroth5  8462  grothprim  8472  sstskm  8480  supsrlem  8749  infm3  9729  nnunb  9977  nnwos  10302  fz1sbc  10875  caubnd  11858  rpnnen2  12520  isprm2  12782  pgpfac1  15331  pgpfac  15335  lidldvgen  16023  iunocv  16597  istopg  16657  dfcon2  17161  1stccn  17205  iskgen3  17260  fbfinnfr  17552  iscmet3  18735  wilthlem3  20324  isch3  21837  choc0  21921  pjnormssi  22764  rabid2f  23151  2reuswap2  23153  ssiun3  23172  rmo3f  23194  rmo4fOLD  23195  mptfnf  23241  sigaclfu2  23497  untuni  24070  dfpo2  24183  dfon2lem8  24217  predreseq  24250  dfrdg4  24560  onsuct0  24952  fates  25058  domfldrefc  25160  ranfldrefc  25161  domrngref  25163  imfstnrelc  25184  qusp  25645  prcnt  25654  bwt2  25695  ismonc  25917  isepic  25927  isconcl7a  26208  nninfnub  26564  n0el  26828  ralxpxfr2d  26863  dford4  27225  ralbidar  27751  rexbidar  27752  stoweidlem52  27904  stoweidlem61  27913  rexrsb  28050  2rmoswap  28065  nbcusgra  28298  cusgrauvtx  28309  ssralv2  28593  en3lpVD  28937  ssralv2VD  28958  trintALTVD  28972  bnj115  29067  bnj538  29085  bnj946  29122  bnj1142  29137  bnj1211  29146  bnj1294  29166  bnj1385  29181  bnj110  29206  bnj611  29266  bnj864  29270  bnj865  29271  bnj1000  29289  bnj978  29297  bnj1049  29320  bnj1090  29325  bnj1133  29335  bnj1176  29351  bnj1186  29353  bnj1253  29363  bnj1388  29379  pmapglbx  30580  cdlemefrs29bpre0  31207
  Copyright terms: Public domain W3C validator