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

Definition df-ral 2549
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 2544 . 2  wff  A. x  e.  A  ph
52cv 1623 . . . . 5  class  x
65, 3wcel 1685 . . . 4  wff  x  e.  A
76, 1wi 6 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1528 . 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  2554  rexnal  2555  ralbida  2558  ralbidv2  2566  ralbii2  2572  r2alf  2579  hbral  2592  hbra1  2593  nfra1  2594  nfrald  2595  r3al  2601  alral  2602  rsp  2604  rgen  2609  rgen2a  2610  ralim  2615  ralimi2  2616  ralimdaa  2621  ralimdv2  2624  ralrimi  2625  r19.21t  2629  ralrimd  2632  r19.21bi  2642  r19.23t  2658  r19.26m  2679  ralcom2  2705  rabid2  2718  rabbi  2719  raleqf  2733  cbvralf  2759  cbvraldva2  2769  ralv  2802  ceqsralt  2812  rspct  2878  rspc  2879  rspcimdv  2886  ralab  2927  ralab2  2931  ralrab2  2932  reu2  2954  reu6  2955  reu3  2956  rmo4  2959  reu8  2962  rmoim  2965  2reuswap  2968  2reu5lem2  2972  2reu5lem3  2973  ra5  3076  rmo2  3077  rmo3  3079  cbvralcsf  3144  dfss3  3171  dfss3f  3173  ssabral  3245  ss2rab  3250  rabss  3251  ssrab  3252  ralunb  3357  reuss2  3449  disj  3496  disj1  3498  r19.2z  3544  r19.3rz  3546  r19.3rzv  3548  ralidm  3558  ralf0  3561  ralsns  3671  unissb  3858  dfint2  3865  elint2  3870  elintrab  3875  ssintrab  3886  dfiin2g  3937  invdisj  4013  disjss3  4023  dftr5  4117  trint  4129  reusv2lem4  4537  find  4680  raliunxp  4824  dmopab3  4890  issref  5055  asymref  5058  asymref2  5059  dffun7  5246  funcnv  5275  funcnvuni  5282  fnres  5325  fnopabg  5332  dff3  5634  dffo3  5636  zfrep6  5709  tfrlem2  6387  nfixp  6830  marypha2lem3  7185  zfregcl  7303  zfinf2  7338  scottexs  7552  scott0s  7553  aceq1  7739  aceq2  7741  kmlem12  7782  kmlem14  7784  kmlem15  7785  zorn2lem4  8121  zorn2lem5  8122  ingru  8432  axgroth5  8441  grothprim  8451  sstskm  8459  supsrlem  8728  infm3  9708  nnunb  9956  nnwos  10281  fz1sbc  10853  caubnd  11836  rpnnen2  12498  isprm2  12760  pgpfac1  15309  pgpfac  15313  lidldvgen  16001  iunocv  16575  istopg  16635  dfcon2  17139  1stccn  17183  iskgen3  17238  fbfinnfr  17530  iscmet3  18713  wilthlem3  20302  isch3  21813  choc0  21897  pjnormssi  22740  untuni  23459  dfpo2  23515  dfon2lem8  23547  predreseq  23580  dfrdg4  23895  onsuct0  24287  fates  24353  domfldrefc  24455  ranfldrefc  24456  domrngref  24458  imfstnrelc  24479  qusp  24941  prcnt  24950  bwt2  24991  ismonc  25213  isepic  25223  isconcl7a  25504  nninfnub  25860  n0el  26124  ralxpxfr2d  26159  dford4  26521  ralbidar  27047  rexbidar  27048  stoweidlem52  27200  stoweidlem61  27209  rexrsb  27326  2rmoswap  27341  ssralv2  27565  en3lpVD  27889  ssralv2VD  27910  trintALTVD  27924  bnj115  28018  bnj538  28036  bnj946  28073  bnj1142  28088  bnj1211  28097  bnj1294  28117  bnj1385  28132  bnj110  28157  bnj611  28217  bnj864  28221  bnj865  28222  bnj1000  28240  bnj978  28248  bnj1049  28271  bnj1090  28276  bnj1133  28286  bnj1176  28302  bnj1186  28304  bnj1253  28314  bnj1388  28330  pmapglbx  29225  cdlemefrs29bpre0  29852
  Copyright terms: Public domain W3C validator