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 2900
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 2895 . 2 wff 𝑥𝐴 𝜑
52cv 1473 . . . . 5 class 𝑥
65, 3wcel 1976 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1472 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 194 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rgen  2905  alral  2911  rsp  2912  r2allem  2920  r3al  2923  nfra1  2924  hbral  2926  nfrald  2927  ral2imi  2930  ralimi2  2932  hbralrimi  2936  r19.21t  2937  ralrimd  2941  r19.21v  2942  ralimdv2  2943  rgen2a  2959  ralbii2  2960  ralbida  2964  ralbidv2  2966  raln  2973  ralnexOLD  2975  r19.23t  3002  r19.26m  3048  ralcom2  3082  rabid2  3095  rabbi  3096  raleqf  3110  cbvralf  3140  cbvraldva2  3150  ralv  3191  ceqsralt  3201  rspct  3274  rspc  3275  rspcimdv  3282  ralxpxfr2d  3297  ralab  3333  ralab2  3337  ralrab2  3338  reu2  3360  reu6  3361  reu3  3362  rmo4  3365  reu8  3368  rmoim  3373  2reuswap  3376  2reu5lem2  3380  2reu5lem3  3381  rmo2  3491  rmo3  3493  cbvralcsf  3530  dfss3  3557  dfss3f  3559  ssabral  3635  ss2rab  3640  rabss  3641  ssrab  3642  ralunb  3755  reuss2  3865  disj  3968  disj1  3970  r19.2z  4011  r19.3rz  4013  ralidm  4026  ralf0  4029  ralf0OLD  4030  rabsssn  4161  ralsnsg  4162  unissb  4399  dfint2  4406  elint2  4411  elintrab  4417  ssintrab  4429  dfiin2g  4483  invdisj  4565  disjss3  4576  dftr5  4677  trint  4690  reusv2lem4  4792  raliunxp  5170  dmopab3  5245  issref  5414  asymref  5417  asymref2  5418  dffun7  5815  funcnv  5857  fnres  5906  mptfnf  5913  fnopabg  5915  dff3  6264  dffo3  6266  find  6960  funcnvuni  6989  zfrep6  7004  nfixp  7790  marypha2lem3  8203  zfregcl  8359  zfregclOLD  8361  zfinf2  8399  scottexs  8610  scott0s  8611  aceq1  8800  aceq2  8802  kmlem12  8843  kmlem14  8845  kmlem15  8846  zorn2lem4  9181  zorn2lem5  9182  ingru  9493  axgroth5  9502  grothprim  9512  sstskm  9520  supsrlem  9788  infm3  10833  nnunb  11137  nnwos  11589  fz1sbc  12242  cotr2g  13511  caubnd  13894  rpnnen2lem12  14741  isprm2  15181  pgpfac1  18250  pgpfac  18254  lidldvgen  19024  iunocv  19791  istopg  20472  dfcon2  20979  1stccn  21023  iskgen3  21109  fbfinnfr  21402  iscmet3  22843  wilthlem3  24540  nbcusgra  25785  cusgrauvtxb  25817  isch3  27275  choc0  27362  pjnormssi  28204  moel  28500  2reuswap2  28505  rmo3f  28512  rmo4fOLD  28513  rabid2f  28517  ssiun3  28552  fmcncfil  29098  bnj115  29838  bnj538OLD  29857  bnj946  29892  bnj1142  29907  bnj1211  29915  bnj1294  29935  bnj1385  29950  bnj110  29975  bnj611  30035  bnj864  30039  bnj865  30040  bnj1000  30058  bnj978  30066  bnj1049  30089  bnj1090  30094  bnj1133  30104  bnj1176  30120  bnj1186  30122  bnj1253  30132  bnj1388  30148  untuni  30633  dfpo2  30691  dfon2lem8  30732  wzel  30808  wzelOLD  30809  dfrdg4  31021  onsuct0  31403  bj-ralvw  31842  bj-ralcom4  31845  poimirlem25  32387  poimirlem30  32392  nninfnub  32500  mptbi12f  32928  n0el  32947  pmapglbx  33856  cdlemefrs29bpre0  34485  dford4  36397  cllem0  36673  elmapintrab  36684  elintima  36747  ss2iundf  36753  ntrneiiso  37192  ntrneik2  37193  ntrneix2  37194  ntrneikb  37195  ralbidar  37453  rexbidar  37454  ssralv2  37541  en3lpVD  37885  ssralv2VD  37907  trintALTVD  37921  ssrabf  38112  rabssf  38117  dffo3f  38142  rexrsb  39601  2rmoswap  39616  falseral0  40092  nrhmzr  41644  empty-surprise  42279  alsconv  42287
  Copyright terms: Public domain W3C validator