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 3101
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 3096 . 2 wff 𝑥𝐴 𝜑
52cv 1636 . . . . 5 class 𝑥
65, 3wcel 2156 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1635 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 197 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  ralanid  3106  rgen  3110  alral  3116  rsp  3117  r2allem  3125  r3al  3128  nfra1  3129  hbral  3131  nfrald  3132  ral2imi  3135  ralimi2  3137  hbralrimi  3142  r19.21t  3143  ralrimd  3147  r19.21v  3148  ralimdv2  3149  rgen2a  3165  ralbii2  3166  ralbida  3170  ralbidv2  3172  raln  3179  r19.23t  3209  r19.26m  3255  ralcom2  3292  rabid2  3307  rabid2f  3308  rabbi  3309  raleqf  3323  cbvralf  3354  cbvraldva2  3364  ralv  3413  ceqsralt  3423  rspct  3495  rspc  3496  rspcimdv  3503  rspc2gv  3514  ralxpxfr2d  3521  ralab  3563  ralab2  3567  ralrab2  3568  reu2  3592  reu6  3593  reu3  3594  rmo4  3597  reu8  3600  rmoim  3605  2reuswap  3608  2reu5lem2  3612  2reu5lem3  3613  rmo2  3721  rmo3  3723  cbvralcsf  3760  dfss3  3787  dfss3f  3790  ssabral  3870  ss2rab  3875  rabss  3876  ssrab  3877  dfdif3  3919  ralunb  3993  reuss2  4108  n0el  4141  disj  4214  disj1  4216  r19.2z  4255  r19.3rz  4257  ralidm  4270  ralf0  4272  falseral0  4274  rabsssn  4408  ralsnsg  4409  unissb  4663  dfint2  4671  elint2  4676  elintrab  4681  ssintrab  4692  dfiin2g  4745  invdisj  4830  disjss3  4843  dftr5  4949  trint  4961  reusv2lem4  5070  raliunxp  5463  dmopab3  5538  idrefOLD  5720  asymref  5723  asymref2  5724  dffun7  6124  funcnv  6165  fnres  6214  mptfnf  6222  fnopabg  6224  dff3  6590  dffo3  6592  find  7317  funcnvuni  7345  zfrep6  7360  nfixp  8160  marypha2lem3  8578  zfregcl  8734  zfinf2  8782  scottexs  8993  scott0s  8994  aceq1  9219  aceq2  9221  kmlem12  9264  kmlem14  9266  kmlem15  9267  zorn2lem4  9602  zorn2lem5  9603  ingru  9918  axgroth5  9927  grothprim  9937  sstskm  9945  supsrlem  10213  infm3  11263  nnunb  11551  nnwos  11970  fz1sbc  12635  cotr2g  13936  caubnd  14317  rpnnen2lem12  15170  isprm2  15609  pgpfac1  18677  pgpfac  18681  lidldvgen  19460  iunocv  20231  istopg  20909  dfconn2  21432  1stccn  21476  iskgen3  21562  fbfinnfr  21854  iscmet3  23299  wilthlem3  25006  isch3  28422  choc0  28509  pjnormssi  29351  moel  29647  2reuswap2  29650  rmo3f  29657  rmo4fOLD  29658  ssiun3  29697  fmcncfil  30298  bnj115  31112  bnj946  31163  bnj1142  31178  bnj1211  31186  bnj1294  31206  bnj1385  31221  bnj110  31246  bnj611  31306  bnj864  31310  bnj865  31311  bnj1000  31329  bnj978  31337  bnj1049  31360  bnj1090  31365  bnj1133  31375  bnj1176  31391  bnj1186  31393  bnj1253  31403  bnj1388  31419  untuni  31903  dfpo2  31962  dfon2lem8  32010  wzel  32085  dfrdg4  32374  onsuct0  32752  bj-ralvw  33168  bj-ralcom4  33171  bj-raldifsn  33360  bj-ismooredr  33370  poimirlem25  33742  poimirlem30  33747  nninfnub  33853  mptbi12f  34280  pmapglbx  35544  cdlemefrs29bpre0  36171  dford4  38091  cllem0  38365  elmapintrab  38376  elintima  38439  ss2iundf  38445  ntrneiiso  38883  ntrneik2  38884  ntrneix2  38885  ntrneikb  38886  ralbidar  39141  rexbidar  39142  ssralv2  39229  en3lpVD  39568  ssralv2VD  39590  trintALTVD  39604  ssrabf  39784  rabssf  39788  dffo3f  39847  rexrsb  41676  2rmoswap  41690  nrhmzr  42435  empty-surprise  43093  alsconv  43101
  Copyright terms: Public domain W3C validator