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

Definition df-ral 2702
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 2697 . 2  wff  A. x  e.  A  ph
52cv 1651 . . . . 5  class  x
65, 3wcel 1725 . . . 4  wff  x  e.  A
76, 1wi 4 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1549 . 2  wff  A. x
( x  e.  A  ->  ph )
94, 8wb 177 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  2707  rexnal  2708  ralbida  2711  ralbidv2  2719  ralbii2  2725  r2alf  2732  hbral  2746  hbra1  2747  nfra1  2748  nfrald  2749  r3al  2755  alral  2756  rsp  2758  rgen  2763  rgen2a  2764  ralim  2769  ralimi2  2770  ralimdaa  2775  ralimdv2  2778  ralrimi  2779  r19.21t  2783  ralrimd  2786  r19.21bi  2796  r19.23t  2812  r19.26m  2833  ralcom2  2864  rabid2  2877  rabbi  2878  raleqf  2892  cbvralf  2918  cbvraldva2  2928  ralv  2961  ceqsralt  2971  rspct  3037  rspc  3038  rspcimdv  3045  ralab  3087  ralab2  3091  ralrab2  3092  reu2  3114  reu6  3115  reu3  3116  rmo4  3119  reu8  3122  rmoim  3125  2reuswap  3128  2reu5lem2  3132  2reu5lem3  3133  ra5  3237  rmo2  3238  rmo3  3240  cbvralcsf  3303  dfss3  3330  dfss3f  3332  ssabral  3406  ss2rab  3411  rabss  3412  ssrab  3413  ralunb  3520  reuss2  3613  disj  3660  disj1  3662  r19.2z  3709  r19.3rz  3711  r19.3rzv  3713  ralidm  3723  ralf0  3726  ralsns  3836  unissb  4037  dfint2  4044  elint2  4049  elintrab  4054  ssintrab  4065  dfiin2g  4116  invdisj  4193  disjss3  4203  dftr5  4297  trint  4309  reusv2lem4  4718  find  4861  raliunxp  5005  dmopab3  5073  issref  5238  asymref  5241  asymref2  5242  dffun7  5470  funcnv  5502  funcnvuni  5509  fnres  5552  fnopabg  5559  dff3  5873  dffo3  5875  zfrep6  5959  tfrlem2  6628  nfixp  7072  marypha2lem3  7433  zfregcl  7551  zfinf2  7586  scottexs  7800  scott0s  7801  aceq1  7987  aceq2  7989  kmlem12  8030  kmlem14  8032  kmlem15  8033  zorn2lem4  8368  zorn2lem5  8369  ingru  8679  axgroth5  8688  grothprim  8698  sstskm  8706  supsrlem  8975  infm3  9956  nnunb  10206  nnwos  10533  fz1sbc  11112  caubnd  12150  rpnnen2  12813  isprm2  13075  pgpfac1  15626  pgpfac  15630  lidldvgen  16314  iunocv  16896  istopg  16956  bwth  17461  dfcon2  17470  1stccn  17514  iskgen3  17569  fbfinnfr  17861  iscmet3  19234  wilthlem3  20841  nbcusgra  21460  cusgrauvtxb  21493  isch3  22732  choc0  22816  pjnormssi  23659  rabid2f  23955  2reuswap2  23963  rmo3f  23970  rmo4fOLD  23971  ssiun3  23997  mptfnf  24061  fmcncfil  24305  untuni  25146  dfpo2  25367  dfon2lem8  25401  predreseq  25434  dfrdg4  25745  onsuct0  26139  nninfnub  26392  n0el  26645  ralxpxfr2d  26678  dford4  27037  ralbidar  27562  rexbidar  27563  rexrsb  27861  2rmoswap  27876  ssralv2  28470  en3lpVD  28811  ssralv2VD  28832  trintALTVD  28846  bnj115  28944  bnj538  28962  bnj946  28999  bnj1142  29014  bnj1211  29023  bnj1294  29043  bnj1385  29058  bnj110  29083  bnj611  29143  bnj864  29147  bnj865  29148  bnj1000  29166  bnj978  29174  bnj1049  29197  bnj1090  29202  bnj1133  29212  bnj1176  29228  bnj1186  29230  bnj1253  29240  bnj1388  29256  pmapglbx  30405  cdlemefrs29bpre0  31032
  Copyright terms: Public domain W3C validator