Definition df-ral 3059

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 47054 or ralndv2 47055, 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

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wral 3058	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1535	. . . . 5 class 𝑥
6	5, 3	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1534	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3060  raln  3066  alral  3072  ralimi2  3075  ral2imi  3082  ralbii2  3086  ralrexbidOLD  3104  r19.26m  3107  r2allem  3139  hbralrimi  3141  ralimdv2  3160  ralbidv2  3171  r19.21vOLD  3178  r3al  3194  rspw  3233  cbvralvw  3234  rsp  3244  r19.21t  3250  r19.23t  3252  ralrimd  3261  ralbidaOLD  3268  nfra1  3281  ralcom4  3283  ralcom4OLD  3284  nfra2wOLD  3297  cbvralfw  3301  hbral  3305  nfraldw  3306  cbvralsvw  3314  raleqbidvvOLD  3332  cbvraldva2  3345  raleqf  3350  sbralie  3355  cbvralf  3357  rgen2a  3368  nfrald  3369  ralcom2  3374  moelOLD  3402  rabbi  3464  rabid2f  3465  rabid2im  3466  rabid2OLD  3468  ralv  3505  ceqsralt  3513  rspct  3607  rspc  3609  rspcimdv  3611  rspc2gv  3631  ralxpxfr2d  3645  ralab  3699  ralabOLD  3700  ralab2  3705  ralrab2  3706  reu2  3733  reu6  3734  reu3  3735  rmo4  3738  reu8  3741  rmo3f  3742  rmoim  3748  2reuswap  3754  2reuswap2  3755  2reu5lem2  3764  2reu5lem3  3765  2rmoswap  3769  rmo2  3895  rmo3  3897  rmoanim  3902  cbvralcsf  3952  dfss3  3983  dfss3f  3986  ssralv  4063  ssabral  4074  ss2rab  4080  rabss  4081  ssrab  4082  dfdif3OLD  4127  rexdifi  4159  ralunb  4206  reuss2  4331  rspn0  4361  n0el  4369  disj  4455  disj1  4457  r19.2z  4500  r19.3rz  4502  ralidmw  4513  rzal  4514  ralidm  4517  ralf0  4519  falseral0  4521  rabsssn  4672  ralsnsg  4674  ralsng  4679  unissb  4943  unissbOLD  4944  dfint2  4952  elint2  4957  elintrab  4964  ssintrab  4975  dfiin2g  5036  invdisj  5133  disjss3  5146  dftr5  5268  dftr5OLD  5269  reusv2lem4  5406  axprlem2  5429  axprlem4  5431  axprlem4OLD  5434  axprlem5OLD  5435  dffr6  5643  raliunxp  5852  dmopab3  5932  rnopab3  5969  asymref  6138  asymref2  6139  dfpo2  6317  dffun7  6594  funcnv  6636  fnres  6695  mptfnf  6703  fnopabg  6705  dff3  7119  dffo3  7121  dffo3f  7125  fnssintima  7381  imaeqalov  7671  find  7917  funcnvuni  7954  zfrep6  7977  ralxp3f  8160  frpoins3xpg  8163  frpoins3xp3g  8164  nfixpw  8954  nfixp  8955  marypha2lem3  9474  zfregcl  9631  zfinf2  9679  scottexs  9924  scott0s  9925  aceq1  10154  aceq2  10156  kmlem12  10199  kmlem14  10201  kmlem15  10202  zorn2lem4  10536  zorn2lem5  10537  ingru  10852  axgroth5  10861  grothprim  10871  sstskm  10879  supsrlem  11148  infm3  12224  nnunb  12519  nnwos  12954  fz1sbc  13636  cotr2g  15011  caubnd  15393  rpnnen2lem12  16257  isprm2  16715  pgpfac1  20114  pgpfac  20118  nrhmzr  20553  lidldvgen  21361  iunocv  21716  ismhp3  22163  istopg  22916  dfconn2  23442  1stccn  23486  iskgen3  23572  fbfinnfr  23864  iscmet3  25340  wilthlem3  27127  eqscut2  27865  elons2  28295  isch3  31269  choc0  31354  pjnormssi  32196  reuxfrdf  32518  rabsspr  32528  rabsstp  32529  inpr0  32557  ssiun3  32578  ssdifidlprm  33465  fmcncfil  33891  bnj115  34717  bnj946  34766  bnj1142  34781  bnj1211  34789  bnj1294  34809  bnj1385  34824  bnj110  34850  bnj611  34910  bnj864  34914  bnj865  34915  bnj1000  34933  bnj978  34941  bnj1049  34966  bnj1090  34971  bnj1133  34981  bnj1176  34997  bnj1186  34999  bnj1253  35009  bnj1388  35025  untuni  35688  dfon2lem8  35771  wzel  35805  dfrdg4  35932  ixpeq12dv  36198  cbvralvw2  36208  onsuct0  36423  bj-ralvw  36861  bj-rcleqf  37007  exrecfnlem  37361  fvineqsneq  37394  poimirlem25  37631  poimirlem30  37636  nninfnub  37737  mptbi12f  38152  pmapglbx  39751  cdlemefrs29bpre0  40378  sn-axrep5v  42233  dford4  43017  unielss  43206  orddif0suc  43257  cllem0  43555  elmapintrab  43565  elintima  43642  ss2iundf  43648  ntrneiiso  44080  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  scottabf  44235  expandral  44285  ismnushort  44296  ralbidar  44440  rexbidar  44441  ssralv2  44528  en3lpVD  44842  ssralv2VD  44863  trintALTVD  44877  traxext  44937  ssrabf  45053  rabssf  45058  r19.3rzf  45100  rexrsb  47049  empty-surprise  49012  alsconv  49020