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 46272 or ralndv2 46273, 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 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1538	. 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  3141  hbralrimi  3143  ralimdv2  3162  ralbidv2  3172  r19.21vOLD  3179  r3al  3195  rspw  3232  cbvralvw  3233  rsp  3243  r19.21t  3249  r19.23t  3251  ralrimd  3260  ralbidaOLD  3267  nfra1  3280  ralcom4  3282  ralcom4OLD  3283  nfra2wOLD  3296  cbvralfw  3300  hbral  3304  nfraldw  3305  nfraldwOLD  3317  cbvralfwOLD  3319  raleqbidvvOLD  3329  raleleq  3336  cbvraldva2  3343  raleqf  3348  sbralie  3353  cbvralf  3355  rgen2a  3366  nfrald  3367  ralcom2  3372  moelOLD  3400  rabbi  3461  rabid2f  3462  rabid2OLD  3464  ralv  3498  ceqsralt  3506  rspct  3598  rspc  3600  rspcimdv  3602  rspc2gv  3621  ralxpxfr2d  3634  ralab  3687  ralabOLD  3688  ralab2  3693  ralrab2  3694  reu2  3721  reu6  3722  reu3  3723  rmo4  3726  reu8  3729  rmo3f  3730  rmoim  3736  2reuswap  3742  2reuswap2  3743  2reu5lem2  3752  2reu5lem3  3753  2rmoswap  3757  rmo2  3881  rmo3  3883  rmoanim  3888  cbvralcsf  3938  dfss3  3970  dfss3f  3973  ssabral  4059  ss2rab  4068  rabss  4069  ssrab  4070  dfdif3  4114  rexdifi  4145  ralunb  4191  reuss2  4315  rspn0  4352  n0el  4361  disj  4447  disjOLD  4448  disj1  4450  r19.2z  4494  r19.3rz  4496  ralidmw  4507  rzal  4508  ralidm  4511  ralf0  4513  ralidmOLD  4515  ralf0OLD  4517  falseral0  4519  rabsssn  4670  ralsnsg  4672  ralsng  4677  unissb  4943  unissbOLD  4944  dfint2  4952  elint2  4957  elintrab  4964  ssintrab  4975  dfiin2g  5035  invdisj  5132  disjss3  5147  dftr5  5269  dftr5OLD  5270  reusv2lem4  5399  axprlem2  5422  axprlem4  5424  axprlem5  5425  dffr6  5634  raliunxp  5839  dmopab3  5919  asymref  6117  asymref2  6118  dfpo2  6295  dffun7  6575  funcnv  6617  fnres  6677  mptfnf  6685  fnopabg  6687  dff3  7101  dffo3  7103  dffo3f  7107  fnssintima  7362  imaeqalov  7650  find  7891  findOLD  7892  funcnvuni  7926  zfrep6  7945  ralxp3f  8128  frpoins3xpg  8131  frpoins3xp3g  8132  nfixpw  8916  nfixp  8917  marypha2lem3  9438  zfregcl  9595  zfinf2  9643  scottexs  9888  scott0s  9889  aceq1  10118  aceq2  10120  kmlem12  10162  kmlem14  10164  kmlem15  10165  zorn2lem4  10500  zorn2lem5  10501  ingru  10816  axgroth5  10825  grothprim  10835  sstskm  10843  supsrlem  11112  infm3  12180  nnunb  12475  nnwos  12906  fz1sbc  13584  cotr2g  14930  caubnd  15312  rpnnen2lem12  16175  isprm2  16626  pgpfac1  19998  pgpfac  20002  nrhmzr  20433  lidldvgen  21182  iunocv  21544  ismhp3  21995  istopg  22717  dfconn2  23243  1stccn  23287  iskgen3  23373  fbfinnfr  23665  iscmet3  25141  wilthlem3  26915  eqscut2  27652  elons2  28064  isch3  30927  choc0  31012  pjnormssi  31854  reuxfrdf  32164  inpr0  32202  ssiun3  32223  fmcncfil  33375  bnj115  34200  bnj946  34249  bnj1142  34264  bnj1211  34272  bnj1294  34292  bnj1385  34307  bnj110  34333  bnj611  34393  bnj864  34397  bnj865  34398  bnj1000  34416  bnj978  34424  bnj1049  34449  bnj1090  34454  bnj1133  34464  bnj1176  34480  bnj1186  34482  bnj1253  34492  bnj1388  34508  untuni  35148  dfon2lem8  35232  wzel  35266  dfrdg4  35393  onsuct0  35790  bj-ralvw  36223  bj-rcleqf  36370  exrecfnlem  36724  fvineqsneq  36757  poimirlem25  36977  poimirlem30  36982  nninfnub  37083  mptbi12f  37498  pmapglbx  39104  cdlemefrs29bpre0  39731  sn-axrep5v  41500  dford4  42231  unielss  42430  orddif0suc  42481  cllem0  42780  elmapintrab  42790  elintima  42867  ss2iundf  42873  ntrneiiso  43305  ntrneik2  43306  ntrneix2  43307  ntrneikb  43308  scottabf  43462  expandral  43512  ismnushort  43523  ralbidar  43667  rexbidar  43668  ssralv2  43755  en3lpVD  44069  ssralv2VD  44090  trintALTVD  44104  ssrabf  44265  rabssf  44270  r19.3rzf  44314  rexrsb  46267  empty-surprise  47991  alsconv  47999