Definition df-ral 3061

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 45457 or ralndv2 45458, 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 3060	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2106	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1539	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 205	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3062  raln  3068  alral  3074  ralimi2  3077  ral2imi  3084  ralbii2  3088  ralrexbidOLD  3106  r19.26m  3109  r2allem  3135  hbralrimi  3137  ralimdv2  3156  ralbidv2  3166  r19.21vOLD  3173  r3al  3189  rspw  3222  cbvralvw  3223  rsp  3228  r19.21t  3234  r19.23t  3236  ralrimd  3245  ralbidaOLD  3252  nfra1  3265  ralcom4  3267  ralcom4OLD  3268  nfra2wOLD  3281  cbvralfw  3285  hbral  3289  nfraldw  3290  nfraldwOLD  3300  cbvralfwOLD  3302  raleqbidvv  3303  cbvraldva2  3321  raleqf  3326  cbvralf  3331  rgen2a  3342  nfrald  3343  ralcom2  3348  moelOLD  3376  rabbi  3430  rabid2f  3436  rabid2OLD  3438  ralv  3470  ceqsralt  3477  rspct  3568  rspc  3570  rspcimdv  3572  rspc2gv  3590  ralxpxfr2d  3599  ralab  3652  ralabOLD  3653  ralab2  3658  ralrab2  3659  reu2  3686  reu6  3687  reu3  3688  rmo4  3691  reu8  3694  rmo3f  3695  rmoim  3701  2reuswap  3707  2reuswap2  3708  2reu5lem2  3717  2reu5lem3  3718  2rmoswap  3722  rmo2  3846  rmo3  3848  rmoanim  3853  cbvralcsf  3903  dfss3  3935  dfss3f  3938  ssabral  4024  ss2rab  4033  rabss  4034  ssrab  4035  dfdif3  4079  rexdifi  4110  ralunb  4156  reuss2  4280  rspn0  4317  n0el  4326  disj  4412  disjOLD  4413  disj1  4415  r19.2z  4457  r19.3rz  4459  ralidmw  4470  rzal  4471  ralidm  4474  ralf0  4476  ralidmOLD  4478  ralf0OLD  4480  falseral0  4482  rabsssn  4633  ralsnsg  4634  ralsng  4639  unissb  4905  unissbOLD  4906  dfint2  4914  elint2  4919  elintrab  4926  ssintrab  4937  dfiin2g  4997  invdisj  5094  disjss3  5109  dftr5  5231  dftr5OLD  5232  reusv2lem4  5361  axprlem2  5384  axprlem4  5386  axprlem5  5387  dffr6  5596  raliunxp  5800  dmopab3  5880  asymref  6075  asymref2  6076  dfpo2  6253  dffun7  6533  funcnv  6575  fnres  6633  mptfnf  6641  fnopabg  6643  dff3  7055  dffo3  7057  fnssintima  7312  imaeqalov  7598  find  7838  findOLD  7839  funcnvuni  7873  zfrep6  7892  ralxp3f  8074  frpoins3xpg  8077  frpoins3xp3g  8078  nfixpw  8861  nfixp  8862  marypha2lem3  9382  zfregcl  9539  zfinf2  9587  scottexs  9832  scott0s  9833  aceq1  10062  aceq2  10064  kmlem12  10106  kmlem14  10108  kmlem15  10109  zorn2lem4  10444  zorn2lem5  10445  ingru  10760  axgroth5  10769  grothprim  10779  sstskm  10787  supsrlem  11056  infm3  12123  nnunb  12418  nnwos  12849  fz1sbc  13527  cotr2g  14873  caubnd  15255  rpnnen2lem12  16118  isprm2  16569  pgpfac1  19873  pgpfac  19877  lidldvgen  20784  iunocv  21122  ismhp3  21570  istopg  22281  dfconn2  22807  1stccn  22851  iskgen3  22937  fbfinnfr  23229  iscmet3  24694  wilthlem3  26456  eqscut2  27188  isch3  30246  choc0  30331  pjnormssi  31173  reuxfrdf  31483  inpr0  31523  ssiun3  31544  fmcncfil  32601  bnj115  33426  bnj946  33475  bnj1142  33490  bnj1211  33498  bnj1294  33518  bnj1385  33533  bnj110  33559  bnj611  33619  bnj864  33623  bnj865  33624  bnj1000  33642  bnj978  33650  bnj1049  33675  bnj1090  33680  bnj1133  33690  bnj1176  33706  bnj1186  33708  bnj1253  33718  bnj1388  33734  untuni  34367  dfon2lem8  34451  wzel  34485  dfrdg4  34612  onsuct0  34989  bj-ralvw  35422  bj-rcleqf  35569  exrecfnlem  35923  fvineqsneq  35956  poimirlem25  36176  poimirlem30  36181  nninfnub  36283  mptbi12f  36698  pmapglbx  38305  cdlemefrs29bpre0  38932  sn-axrep5v  40709  dford4  41411  unielss  41610  orddif0suc  41661  cllem0  41960  elmapintrab  41970  elintima  42047  ss2iundf  42053  ntrneiiso  42485  ntrneik2  42486  ntrneix2  42487  ntrneikb  42488  scottabf  42642  expandral  42692  ismnushort  42703  ralbidar  42847  rexbidar  42848  ssralv2  42935  en3lpVD  43249  ssralv2VD  43270  trintALTVD  43284  ssrabf  43446  rabssf  43451  r19.3rzf  43495  dffo3f  43520  rexrsb  45452  nrhmzr  46291  empty-surprise  47349  alsconv  47357