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

Definition df-ral 3111
 Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. Note: This notation is most often used to express that 𝜑 holds for all elements of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather focus on those 𝑥 that happen to be contained in the corresponding 𝐴(𝑥). This hardly used interpretation could still occur naturally. For some examples, look at ralndv1 43704 or ralndv2 43705, courtesy of AV. So be careful to either keep 𝐴 independent of 𝑥, or adjust your comments to include such exotic cases. (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 3106 . 2 wff 𝑥𝐴 𝜑
52cv 1537 . . . . 5 class 𝑥
65, 3wcel 2111 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1536 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 209 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
 Colors of variables: wff setvar class This definition is referenced by:  rgen  3116  alral  3122  raln  3123  ral2imi  3124  ralimi2  3125  ralbii2  3131  r19.26m  3140  r19.21v  3142  ralimdv2  3143  hbralrimi  3147  ralbidv2  3160  r2allem  3165  r3al  3167  rsp  3170  r19.21t  3178  ralrimd  3182  nfra1  3183  hbral  3185  nfraldw  3187  nfrald  3188  rgen2a  3193  ralbida  3194  ralcom4  3198  r19.23t  3272  ralrexbid  3281  ralcom2  3316  rabid2  3334  rabid2f  3335  rabbi  3336  raleqf  3350  cbvralfw  3382  cbvralfwOLD  3383  cbvralf  3385  cbvralvw  3396  cbvraldva2  3403  ralv  3466  ceqsralt  3475  rspct  3557  rspc  3559  rspcimdv  3561  rspc2gv  3580  ralxpxfr2d  3587  ralab  3632  ralab2  3636  ralab2OLD  3637  ralrab2  3638  reu2  3664  reu6  3665  reu3  3666  rmo4  3669  reu8  3672  rmo3f  3673  rmoim  3679  2reuswap  3685  2reuswap2  3686  2reu5lem2  3695  2reu5lem3  3696  2rmoswap  3700  rmo2  3816  rmo3  3818  rmoanim  3823  cbvralcsf  3870  dfss3  3903  dfss3f  3906  ssabral  3990  ss2rab  3998  rabss  3999  ssrab  4000  dfdif3  4042  rexdifi  4073  ralunb  4118  reuss2  4235  rspn0  4266  n0el  4275  disj  4355  disjOLD  4356  disj1  4358  r19.2z  4398  r19.3rz  4400  ralidm  4413  ralf0  4415  falseral0  4417  rabsssn  4567  ralsnsg  4568  unissb  4833  dfint2  4841  elint2  4846  elintrab  4851  ssintrab  4862  dfiin2g  4920  invdisj  5015  disjss3  5030  dftr5  5140  reusv2lem4  5268  axprlem2  5291  axprlem4  5293  axprlem5  5294  raliunxp  5675  dmopab3  5753  asymref  5944  asymref2  5945  dffun7  6352  funcnv  6394  fnres  6447  mptfnf  6456  fnopabg  6458  dff3  6844  dffo3  6846  find  7590  findOLD  7591  funcnvuni  7621  zfrep6  7641  nfixpw  8466  nfixp  8467  marypha2lem3  8888  zfregcl  9045  zfinf2  9092  scottexs  9303  scott0s  9304  aceq1  9531  aceq2  9533  kmlem12  9575  kmlem14  9577  kmlem15  9578  zorn2lem4  9913  zorn2lem5  9914  ingru  10229  axgroth5  10238  grothprim  10248  sstskm  10256  supsrlem  10525  infm3  11590  nnunb  11884  nnwos  12306  fz1sbc  12981  cotr2g  14330  caubnd  14713  rpnnen2lem12  15573  isprm2  16019  pgpfac1  19199  pgpfac  19203  lidldvgen  20025  iunocv  20375  ismhp3  20801  istopg  21510  dfconn2  22034  1stccn  22078  iskgen3  22164  fbfinnfr  22456  iscmet3  23907  wilthlem3  25665  isch3  29034  choc0  29119  pjnormssi  29961  nelbOLD  30249  moel  30269  reuxfrdf  30272  inpr0  30314  ssiun3  30332  fmcncfil  31299  bnj115  32120  bnj946  32171  bnj1142  32186  bnj1211  32194  bnj1294  32214  bnj1385  32229  bnj110  32255  bnj611  32315  bnj864  32319  bnj865  32320  bnj1000  32338  bnj978  32346  bnj1049  32371  bnj1090  32376  bnj1133  32386  bnj1176  32402  bnj1186  32404  bnj1253  32414  bnj1388  32430  untuni  33063  dfpo2  33119  dfon2lem8  33163  wzel  33239  dfrdg4  33540  onsuct0  33917  bj-ralvw  34338  bj-rcleqf  34480  exrecfnlem  34815  fvineqsneq  34848  poimirlem25  35101  poimirlem30  35106  nninfnub  35208  mptbi12f  35623  pmapglbx  37084  cdlemefrs29bpre0  37711  sn-axrep5v  39419  dford4  40013  cllem0  40308  elmapintrab  40319  elintima  40397  ss2iundf  40403  ntrneiiso  40837  ntrneik2  40838  ntrneix2  40839  ntrneikb  40840  scottabf  40991  expandral  41041  ralbidar  41192  rexbidar  41193  ssralv2  41280  en3lpVD  41594  ssralv2VD  41615  trintALTVD  41629  ssrabf  41793  rabssf  41797  dffo3f  41849  rexrsb  43698  nrhmzr  44540  empty-surprise  45351  alsconv  45359
 Copyright terms: Public domain W3C validator