Definition df-ral 3045

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 47106 or ralndv2 47107, 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 3044	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1538	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3046  raln  3052  alral  3058  ralimi2  3061  ral2imi  3068  ralbii2  3071  r19.26m  3090  r2allem  3121  hbralrimi  3123  ralimdv2  3142  ralbidv2  3152  r19.21vOLD  3159  r3al  3175  rspw  3214  cbvralvw  3215  rsp  3225  r19.21t  3231  r19.23t  3233  ralrimd  3242  nfra1  3261  ralcom4  3263  cbvralfw  3278  hbral  3282  nfraldw  3283  cbvralsvw  3290  raleqbidvvOLD  3308  cbvraldva2  3321  sbralie  3326  sbralieOLD  3328  raleqf  3329  cbvralf  3334  rgen2a  3345  nfrald  3346  ralcom2  3351  rabbi  3436  rabid2f  3437  rabid2im  3438  ralv  3474  ceqsralt  3482  rspct  3574  rspc  3576  rspcimdv  3578  rspc2gv  3598  ralxpxfr2d  3612  ralab  3664  ralab2  3668  ralrab2  3669  reu2  3696  reu6  3697  reu3  3698  rmo4  3701  reu8  3704  rmo3f  3705  rmoim  3711  2reuswap  3717  2reuswap2  3718  2reu5lem2  3727  2reu5lem3  3728  2rmoswap  3732  rmo2  3850  rmo3  3852  rmoanim  3857  cbvralcsf  3904  dfss3  3935  dfss3f  3938  ssralv  4015  ralss  4021  ssabral  4028  ss2rab  4034  rabss  4035  ssrab  4036  dfdif3OLD  4081  rexdifi  4113  ralunb  4160  reuss2  4289  rspn0  4319  n0el  4327  disj  4413  disj1  4415  r19.2z  4458  r19.3rz  4460  ralidmw  4471  rzal  4472  ralidm  4475  ralf0  4477  falseral0  4479  rabsssn  4632  ralsnsg  4634  ralsng  4639  unissb  4903  unissbOLD  4904  dfint2  4912  elint2  4917  elintrab  4924  ssintrab  4935  dfiin2g  4996  invdisj  5093  disjss3  5106  dftr5  5218  dftr5OLD  5219  reusv2lem4  5356  axprlem2  5379  axprlem4  5381  axprlem4OLD  5384  axprlem5OLD  5385  dffr6  5594  raliunxp  5803  dmopab3  5883  rnopab3  5920  asymref  6089  asymref2  6090  dfpo2  6269  dffun7  6543  funcnv  6585  fnres  6645  mptfnf  6653  fnopabg  6655  dff3  7072  dffo3  7074  dffo3f  7078  fnssintima  7337  imaeqalov  7628  find  7871  funcnvuni  7908  zfrep6  7933  ralxp3f  8116  frpoins3xpg  8119  frpoins3xp3g  8120  nfixpw  8889  nfixp  8890  marypha2lem3  9388  zfregcl  9547  zfinf2  9595  scottexs  9840  scott0s  9841  aceq1  10070  aceq2  10072  kmlem12  10115  kmlem14  10117  kmlem15  10118  zorn2lem4  10452  zorn2lem5  10453  ingru  10768  axgroth5  10777  grothprim  10787  sstskm  10795  supsrlem  11064  infm3  12142  nnunb  12438  nnwos  12874  fz1sbc  13561  cotr2g  14942  caubnd  15325  rpnnen2lem12  16193  isprm2  16652  pgpfac1  20012  pgpfac  20016  nrhmzr  20446  lidldvgen  21244  iunocv  21590  ismhp3  22029  istopg  22782  dfconn2  23306  1stccn  23350  iskgen3  23436  fbfinnfr  23728  iscmet3  25193  wilthlem3  26980  eqscut2  27718  elons2  28159  onsfi  28247  isch3  31170  choc0  31255  pjnormssi  32097  reuxfrdf  32420  rabsspr  32430  rabsstp  32431  inpr0  32461  ssiun3  32487  ssdifidlprm  33429  fmcncfil  33921  bnj115  34715  bnj946  34764  bnj1142  34779  bnj1211  34787  bnj1294  34807  bnj1385  34822  bnj110  34848  bnj611  34908  bnj864  34912  bnj865  34913  bnj1000  34931  bnj978  34939  bnj1049  34964  bnj1090  34969  bnj1133  34979  bnj1176  34995  bnj1186  34997  bnj1253  35007  bnj1388  35023  onvf1odlem4  35093  untuni  35696  dfon2lem8  35778  wzel  35812  dfrdg4  35939  ixpeq12dv  36204  cbvralvw2  36214  onsuct0  36429  bj-ralvw  36867  bj-rcleqf  37013  exrecfnlem  37367  fvineqsneq  37400  poimirlem25  37639  poimirlem30  37644  nninfnub  37745  mptbi12f  38160  eqab2  38237  pmapglbx  39763  cdlemefrs29bpre0  40390  sn-axrep5v  42204  dford4  43018  unielss  43207  orddif0suc  43257  cllem0  43555  elmapintrab  43565  elintima  43642  ss2iundf  43648  ntrneiiso  44080  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  scottabf  44229  expandral  44279  ismnushort  44290  ralbidar  44434  rexbidar  44435  ssralv2  44521  en3lpVD  44834  ssralv2VD  44855  trintALTVD  44869  traxext  44967  dfac5prim  44980  permac8prim  45004  nregmodel  45007  ssrabf  45108  rabssf  45113  r19.3rzf  45152  rexrsb  47101  empty-surprise  49771  alsconv  49779