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 2901
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 2896 . 2 wff 𝑥𝐴 𝜑
52cv 1474 . . . . 5 class 𝑥
65, 3wcel 1977 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1473 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 195 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rgen  2906  alral  2912  rsp  2913  r2allem  2921  r3al  2924  nfra1  2925  hbral  2927  nfrald  2928  ral2imi  2931  ralimi2  2933  hbralrimi  2937  r19.21t  2938  ralrimd  2942  r19.21v  2943  ralimdv2  2944  rgen2a  2960  ralbii2  2961  ralbida  2965  ralbidv2  2967  raln  2974  ralnexOLD  2976  r19.23t  3003  r19.26m  3049  ralcom2  3083  rabid2  3096  rabbi  3097  raleqf  3111  cbvralf  3141  cbvraldva2  3151  ralv  3192  ceqsralt  3202  rspct  3275  rspc  3276  rspcimdv  3283  ralxpxfr2d  3298  ralab  3334  ralab2  3338  ralrab2  3339  reu2  3361  reu6  3362  reu3  3363  rmo4  3366  reu8  3369  rmoim  3374  2reuswap  3377  2reu5lem2  3381  2reu5lem3  3382  rmo2  3492  rmo3  3494  cbvralcsf  3531  dfss3  3558  dfss3f  3560  ssabral  3636  ss2rab  3641  rabss  3642  ssrab  3643  ralunb  3756  reuss2  3866  disj  3969  disj1  3971  r19.2z  4012  r19.3rz  4014  ralidm  4027  ralf0  4030  ralf0OLD  4031  rabsssn  4162  ralsnsg  4163  unissb  4405  dfint2  4412  elint2  4417  elintrab  4423  ssintrab  4435  dfiin2g  4489  invdisj  4571  disjss3  4582  dftr5  4683  trint  4696  reusv2lem4  4798  raliunxp  5183  dmopab3  5259  issref  5428  asymref  5431  asymref2  5432  dffun7  5830  funcnv  5872  fnres  5921  mptfnf  5928  fnopabg  5930  dff3  6280  dffo3  6282  find  6983  funcnvuni  7012  zfrep6  7027  nfixp  7813  marypha2lem3  8226  zfregcl  8382  zfregclOLD  8384  zfinf2  8422  scottexs  8633  scott0s  8634  aceq1  8823  aceq2  8825  kmlem12  8866  kmlem14  8868  kmlem15  8869  zorn2lem4  9204  zorn2lem5  9205  ingru  9516  axgroth5  9525  grothprim  9535  sstskm  9543  supsrlem  9811  infm3  10861  nnunb  11165  nnwos  11631  fz1sbc  12285  cotr2g  13563  caubnd  13946  rpnnen2lem12  14793  isprm2  15233  pgpfac1  18302  pgpfac  18306  lidldvgen  19076  iunocv  19844  istopg  20525  dfcon2  21032  1stccn  21076  iskgen3  21162  fbfinnfr  21455  iscmet3  22899  wilthlem3  24596  nbcusgra  25992  cusgrauvtxb  26024  isch3  27482  choc0  27569  pjnormssi  28411  moel  28707  2reuswap2  28712  rmo3f  28719  rmo4fOLD  28720  rabid2f  28724  ssiun3  28759  fmcncfil  29305  bnj115  30045  bnj538OLD  30064  bnj946  30099  bnj1142  30114  bnj1211  30122  bnj1294  30142  bnj1385  30157  bnj110  30182  bnj611  30242  bnj864  30246  bnj865  30247  bnj1000  30265  bnj978  30273  bnj1049  30296  bnj1090  30301  bnj1133  30311  bnj1176  30327  bnj1186  30329  bnj1253  30339  bnj1388  30355  untuni  30840  dfpo2  30898  dfon2lem8  30939  wzel  31015  wzelOLD  31016  dfrdg4  31228  onsuct0  31610  bj-ralvw  32059  bj-ralcom4  32062  poimirlem25  32604  poimirlem30  32609  nninfnub  32717  mptbi12f  33145  n0el  33164  pmapglbx  34073  cdlemefrs29bpre0  34702  dford4  36614  cllem0  36890  elmapintrab  36901  elintima  36964  ss2iundf  36970  ntrneiiso  37409  ntrneik2  37410  ntrneix2  37411  ntrneikb  37412  ralbidar  37670  rexbidar  37671  ssralv2  37758  en3lpVD  38102  ssralv2VD  38124  trintALTVD  38138  ssrabf  38329  rabssf  38334  dffo3f  38359  rexrsb  39818  2rmoswap  39833  falseral0  40308  nrhmzr  41663  empty-surprise  42337  alsconv  42345
  Copyright terms: Public domain W3C validator