Definition df-ral 3046

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 47110 or ralndv2 47111, 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 3045	. 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  3047  raln  3053  alral  3059  ralimi2  3062  ral2imi  3069  ralbii2  3072  r19.26m  3091  r2allem  3122  hbralrimi  3124  ralimdv2  3143  ralbidv2  3153  r19.21vOLD  3160  r3al  3176  rspw  3215  cbvralvw  3216  rsp  3226  r19.21t  3232  r19.23t  3234  ralrimd  3243  nfra1  3262  ralcom4  3264  cbvralfw  3280  hbral  3284  nfraldw  3285  cbvralsvw  3292  raleqbidvvOLD  3310  cbvraldva2  3323  sbralie  3328  sbralieOLD  3330  raleqf  3331  cbvralf  3336  rgen2a  3347  nfrald  3348  ralcom2  3353  rabbi  3439  rabid2f  3440  rabid2im  3441  ralv  3477  ceqsralt  3485  rspct  3577  rspc  3579  rspcimdv  3581  rspc2gv  3601  ralxpxfr2d  3615  ralab  3667  ralab2  3671  ralrab2  3672  reu2  3699  reu6  3700  reu3  3701  rmo4  3704  reu8  3707  rmo3f  3708  rmoim  3714  2reuswap  3720  2reuswap2  3721  2reu5lem2  3730  2reu5lem3  3731  2rmoswap  3735  rmo2  3853  rmo3  3855  rmoanim  3860  cbvralcsf  3907  dfss3  3938  dfss3f  3941  ssralv  4018  ralss  4024  ssabral  4031  ss2rab  4037  rabss  4038  ssrab  4039  dfdif3OLD  4084  rexdifi  4116  ralunb  4163  reuss2  4292  rspn0  4322  n0el  4330  disj  4416  disj1  4418  r19.2z  4461  r19.3rz  4463  ralidmw  4474  rzal  4475  ralidm  4478  ralf0  4480  falseral0  4482  rabsssn  4635  ralsnsg  4637  ralsng  4642  unissb  4906  unissbOLD  4907  dfint2  4915  elint2  4920  elintrab  4927  ssintrab  4938  dfiin2g  4999  invdisj  5096  disjss3  5109  dftr5  5221  dftr5OLD  5222  reusv2lem4  5359  axprlem2  5382  axprlem4  5384  axprlem4OLD  5387  axprlem5OLD  5388  dffr6  5597  raliunxp  5806  dmopab3  5886  rnopab3  5923  asymref  6092  asymref2  6093  dfpo2  6272  dffun7  6546  funcnv  6588  fnres  6648  mptfnf  6656  fnopabg  6658  dff3  7075  dffo3  7077  dffo3f  7081  fnssintima  7340  imaeqalov  7631  find  7874  funcnvuni  7911  zfrep6  7936  ralxp3f  8119  frpoins3xpg  8122  frpoins3xp3g  8123  nfixpw  8892  nfixp  8893  marypha2lem3  9395  zfregcl  9554  zfinf2  9602  scottexs  9847  scott0s  9848  aceq1  10077  aceq2  10079  kmlem12  10122  kmlem14  10124  kmlem15  10125  zorn2lem4  10459  zorn2lem5  10460  ingru  10775  axgroth5  10784  grothprim  10794  sstskm  10802  supsrlem  11071  infm3  12149  nnunb  12445  nnwos  12881  fz1sbc  13568  cotr2g  14949  caubnd  15332  rpnnen2lem12  16200  isprm2  16659  pgpfac1  20019  pgpfac  20023  nrhmzr  20453  lidldvgen  21251  iunocv  21597  ismhp3  22036  istopg  22789  dfconn2  23313  1stccn  23357  iskgen3  23443  fbfinnfr  23735  iscmet3  25200  wilthlem3  26987  eqscut2  27725  elons2  28166  onsfi  28254  isch3  31177  choc0  31262  pjnormssi  32104  reuxfrdf  32427  rabsspr  32437  rabsstp  32438  inpr0  32468  ssiun3  32494  ssdifidlprm  33436  fmcncfil  33928  bnj115  34722  bnj946  34771  bnj1142  34786  bnj1211  34794  bnj1294  34814  bnj1385  34829  bnj110  34855  bnj611  34915  bnj864  34919  bnj865  34920  bnj1000  34938  bnj978  34946  bnj1049  34971  bnj1090  34976  bnj1133  34986  bnj1176  35002  bnj1186  35004  bnj1253  35014  bnj1388  35030  onvf1odlem4  35100  untuni  35703  dfon2lem8  35785  wzel  35819  dfrdg4  35946  ixpeq12dv  36211  cbvralvw2  36221  onsuct0  36436  bj-ralvw  36874  bj-rcleqf  37020  exrecfnlem  37374  fvineqsneq  37407  poimirlem25  37646  poimirlem30  37651  nninfnub  37752  mptbi12f  38167  eqab2  38244  pmapglbx  39770  cdlemefrs29bpre0  40397  sn-axrep5v  42211  dford4  43025  unielss  43214  orddif0suc  43264  cllem0  43562  elmapintrab  43572  elintima  43649  ss2iundf  43655  ntrneiiso  44087  ntrneik2  44088  ntrneix2  44089  ntrneikb  44090  scottabf  44236  expandral  44286  ismnushort  44297  ralbidar  44441  rexbidar  44442  ssralv2  44528  en3lpVD  44841  ssralv2VD  44862  trintALTVD  44876  traxext  44974  dfac5prim  44987  permac8prim  45011  nregmodel  45014  ssrabf  45115  rabssf  45120  r19.3rzf  45159  rexrsb  47105  empty-surprise  49775  alsconv  49783