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

Definition df-ral 2913
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 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-ral
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wral 2908 . 2 wff 𝑥𝐴 𝜑
52cv 1479 . . . . 5 class 𝑥
65, 3wcel 1987 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1478 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rgen  2918  alral  2924  rsp  2925  r2allem  2933  r3al  2936  nfra1  2937  hbral  2939  nfrald  2940  ral2imi  2943  ralimi2  2945  hbralrimi  2950  r19.21t  2951  ralrimd  2955  r19.21v  2956  ralimdv2  2957  rgen2a  2973  ralbii2  2974  ralbida  2978  ralbidv2  2980  raln  2987  ralnexOLD  2989  r19.23t  3016  r19.26m  3062  ralcom2  3098  rabid2  3111  rabid2f  3112  rabbi  3113  raleqf  3127  cbvralf  3157  cbvraldva2  3167  ralv  3209  ceqsralt  3219  rspct  3292  rspc  3293  rspcimdv  3300  rspc2gv  3310  ralxpxfr2d  3316  ralab  3354  ralab2  3358  ralrab2  3359  reu2  3381  reu6  3382  reu3  3383  rmo4  3386  reu8  3389  rmoim  3394  2reuswap  3397  2reu5lem2  3401  2reu5lem3  3402  rmo2  3512  rmo3  3514  cbvralcsf  3551  dfss3  3578  dfss3f  3580  ssabral  3658  ss2rab  3663  rabss  3664  ssrab  3665  ralunb  3778  reuss2  3889  disj  3995  disj1  3997  r19.2z  4038  r19.3rz  4040  ralidm  4053  ralf0  4056  ralf0OLD  4057  falseral0  4059  rabsssn  4193  ralsnsg  4194  unissb  4442  dfint2  4449  elint2  4454  elintrab  4460  ssintrab  4472  dfiin2g  4526  invdisj  4611  disjss3  4622  dftr5  4725  trint  4738  reusv2lem4  4842  raliunxp  5231  dmopab3  5307  issref  5478  asymref  5481  asymref2  5482  dffun7  5884  funcnv  5926  fnres  5975  mptfnf  5982  fnopabg  5984  dff3  6338  dffo3  6340  find  7053  funcnvuni  7081  zfrep6  7096  nfixp  7887  marypha2lem3  8303  zfregcl  8459  zfregclOLD  8461  zfinf2  8499  scottexs  8710  scott0s  8711  aceq1  8900  aceq2  8902  kmlem12  8943  kmlem14  8945  kmlem15  8946  zorn2lem4  9281  zorn2lem5  9282  ingru  9597  axgroth5  9606  grothprim  9616  sstskm  9624  supsrlem  9892  infm3  10942  nnunb  11248  nnwos  11715  fz1sbc  12373  cotr2g  13665  caubnd  14048  rpnnen2lem12  14898  isprm2  15338  pgpfac1  18419  pgpfac  18423  lidldvgen  19195  iunocv  19965  istopg  20640  dfconn2  21162  1stccn  21206  iskgen3  21292  fbfinnfr  21585  iscmet3  23031  wilthlem3  24730  isch3  27986  choc0  28073  pjnormssi  28915  moel  29212  2reuswap2  29217  rmo3f  29224  rmo4fOLD  29225  ssiun3  29263  fmcncfil  29801  bnj115  30552  bnj538OLD  30571  bnj946  30606  bnj1142  30621  bnj1211  30629  bnj1294  30649  bnj1385  30664  bnj110  30689  bnj611  30749  bnj864  30753  bnj865  30754  bnj1000  30772  bnj978  30780  bnj1049  30803  bnj1090  30808  bnj1133  30818  bnj1176  30834  bnj1186  30836  bnj1253  30846  bnj1388  30862  untuni  31347  dfpo2  31406  dfon2lem8  31449  wzel  31525  wzelOLD  31526  dfrdg4  31753  onsuct0  32135  bj-ralvw  32565  bj-ralcom4  32568  poimirlem25  33105  poimirlem30  33110  nninfnub  33218  mptbi12f  33646  n0el  33665  pmapglbx  34574  cdlemefrs29bpre0  35203  dford4  37115  cllem0  37391  elmapintrab  37402  elintima  37465  ss2iundf  37471  ntrneiiso  37910  ntrneik2  37911  ntrneix2  37912  ntrneikb  37913  ralbidar  38170  rexbidar  38171  ssralv2  38258  en3lpVD  38602  ssralv2VD  38624  trintALTVD  38638  ssrabf  38822  rabssf  38827  dffo3f  38873  rexrsb  40503  2rmoswap  40518  nrhmzr  41191  empty-surprise  41861  alsconv  41869
  Copyright terms: Public domain W3C validator