Definition df-ral 3143

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 43353 or ralndv2 43354, 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 3138	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1535	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 208	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3148  alral  3154  raln  3155  ral2imi  3156  ralimi2  3157  ralbii2  3163  ralanidOLD  3169  r19.26m  3173  r19.21v  3175  ralimdv2  3176  hbralrimi  3180  ralbidv2  3195  r2allem  3200  r3al  3202  rsp  3205  r19.21t  3214  ralrimd  3218  nfra1  3219  hbral  3221  nfraldw  3223  nfrald  3224  rgen2a  3229  ralbida  3230  ralcom4  3235  r19.23t  3313  ralrexbid  3322  ralcom2  3363  rabid2  3381  rabid2f  3382  rabbi  3383  raleqf  3397  cbvralfw  3437  cbvralf  3439  cbvralvw  3449  cbvraldva2  3456  ralv  3519  ceqsralt  3528  rspct  3609  rspc  3611  rspcimdv  3613  rspc2gv  3632  ralxpxfr2d  3639  ralab  3684  ralab2  3688  ralab2OLD  3689  ralrab2  3690  reu2  3716  reu6  3717  reu3  3718  rmo4  3721  reu8  3724  rmo3f  3725  rmoim  3731  2reuswap  3737  2reuswap2  3738  2reu5lem2  3747  2reu5lem3  3748  2rmoswap  3752  rmo2  3870  rmo3  3872  rmo3OLD  3873  rmoanim  3878  cbvralcsf  3925  dfss3  3956  dfss3f  3959  ssabral  4042  ss2rab  4047  rabss  4048  ssrab  4049  dfdif3  4091  rexdifi  4122  ralunb  4167  reuss2  4283  n0el  4321  disj  4399  disj1  4401  r19.2z  4440  r19.3rz  4442  ralidm  4455  ralf0  4457  falseral0  4459  rabsssn  4607  ralsnsg  4608  unissb  4870  dfint2  4878  elint2  4883  elintrab  4888  ssintrab  4899  dfiin2g  4957  invdisj  5050  disjss3  5065  dftr5  5175  reusv2lem4  5302  axprlem2  5325  axprlem4  5327  axprlem5  5328  raliunxp  5710  dmopab3  5788  asymref  5976  asymref2  5977  dffun7  6382  funcnv  6423  fnres  6474  mptfnf  6483  fnopabg  6485  dff3  6866  dffo3  6868  find  7607  funcnvuni  7636  zfrep6  7656  nfixpw  8480  nfixp  8481  marypha2lem3  8901  zfregcl  9058  zfinf2  9105  scottexs  9316  scott0s  9317  aceq1  9543  aceq2  9545  kmlem12  9587  kmlem14  9589  kmlem15  9590  zorn2lem4  9921  zorn2lem5  9922  ingru  10237  axgroth5  10246  grothprim  10256  sstskm  10264  supsrlem  10533  infm3  11600  nnunb  11894  nnwos  12316  fz1sbc  12984  cotr2g  14336  caubnd  14718  rpnnen2lem12  15578  isprm2  16026  pgpfac1  19202  pgpfac  19206  lidldvgen  20028  iunocv  20825  istopg  21503  dfconn2  22027  1stccn  22071  iskgen3  22157  fbfinnfr  22449  iscmet3  23896  wilthlem3  25647  isch3  29018  choc0  29103  pjnormssi  29945  nelbOLD  30232  moel  30252  reuxfrdf  30255  inpr0  30292  ssiun3  30310  fmcncfil  31174  bnj115  31995  bnj946  32046  bnj1142  32061  bnj1211  32069  bnj1294  32089  bnj1385  32104  bnj110  32130  bnj611  32190  bnj864  32194  bnj865  32195  bnj1000  32213  bnj978  32221  bnj1049  32246  bnj1090  32251  bnj1133  32261  bnj1176  32277  bnj1186  32279  bnj1253  32289  bnj1388  32305  untuni  32935  dfpo2  32991  dfon2lem8  33035  wzel  33111  dfrdg4  33412  onsuct0  33789  bj-ralvw  34198  bj-rcleqf  34340  exrecfnlem  34663  fvineqsneq  34696  poimirlem25  34932  poimirlem30  34937  nninfnub  35041  mptbi12f  35459  pmapglbx  36920  cdlemefrs29bpre0  37547  sn-axrep5v  39157  dford4  39675  cllem0  39974  elmapintrab  39985  elintima  40047  ss2iundf  40053  ntrneiiso  40490  ntrneik2  40491  ntrneix2  40492  ntrneikb  40493  scottabf  40625  expandral  40675  ralbidar  40826  rexbidar  40827  ssralv2  40914  en3lpVD  41228  ssralv2VD  41249  trintALTVD  41263  ssrabf  41430  rabssf  41434  dffo3f  41487  rexrsb  43347  nrhmzr  44193  empty-surprise  44932  alsconv  44940