Definition df-ral 3079

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 47704 or ralndv2 47705, 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 3078	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1561	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1560	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 208	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3080  ralrid  3086  raln  3087  ralimi2  3096  ral2imi  3103  ralbii2  3106  r19.26m  3123  r2allem  3152  ralimdv2  3173  ralbidv2  3183  r3al  3202  rspw  3241  cbvralvw  3242  rsp  3252  r19.21t  3258  r19.23t  3260  ralrimd  3269  nfra1  3288  ralcom4  3290  cbvralfw  3304  hbral  3308  nfraldw  3309  cbvralsvw  3315  cbvraldva2  3340  sbralie  3342  sbralieOLD  3344  raleqf  3345  cbvralf  3349  rgen2a  3360  nfrald  3361  ralcom2  3366  rabbi  3446  rabid2f  3447  rabid2im  3448  ralv  3482  ceqsralt  3490  rspct  3569  rspc  3571  rspcimdv  3573  rspc2gv  3593  ralxpxfr2d  3607  ralab  3658  ralab2  3662  ralrab2  3663  reu2  3690  reu6  3691  reu3  3692  rmo4  3695  reu8  3698  rmo3f  3699  rmoim  3705  2reuswap  3711  2reuswap2  3712  2reu5lem2  3721  2reu5lem3  3722  2rmoswap  3726  rmo2  3842  rmo3  3844  rmoanim  3849  cbvralcsf  3896  dfss3  3927  dfss3f  3930  ssralv  4007  ralss  4011  ssabral  4019  ss2rab  4024  rabss  4025  ssrab  4026  ss2rabd  4027  dfdif3OLD  4074  rexdifi  4105  ralunb  4151  reuss2  4280  rspn0  4311  n0el  4319  disj  4406  disj1  4408  rzal  4450  ralf0  4453  r19.2z  4455  r19.3rz  4457  falseral0OLD  4471  ralidmw  4472  ralidm  4473  rabsssn  4629  ralsnsg  4631  ralsng  4636  unissb  4901  dfint2  4909  elint2  4914  elintrab  4920  ssintrab  4931  dfiin2g  4990  invdisj  5088  disjss3  5101  dftr5  5213  zfrep6  5241  reusv2lem4  5360  axprlem2  5383  axprlem4OLD  5389  axprlem5OLD  5390  dffr6  5605  raliunxp  5813  dmopab3  5897  rnopab3  5934  asymref  6105  asymref2  6106  dfpo2  6285  dffun7  6550  funcnv  6592  fnres  6650  mptfnf  6658  fnopabg  6660  dff3  7083  dffo3  7085  dffo3f  7089  fnssintima  7348  imaeqalov  7637  find  7878  funcnvuni  7915  zfrep6OLD  7938  ralxp3f  8119  frpoins3xpg  8122  frpoins3xp3g  8123  nfixpw  8900  nfixp  8901  marypha2lem3  9385  zfregcl  9544  zfregclOLD  9545  zfinf2  9599  scottexs  9847  scott0s  9848  aceq1  10075  aceq2  10077  kmlem12  10120  kmlem14  10122  kmlem15  10123  zorn2lem4  10458  zorn2lem5  10459  axgroth5  10784  grothprim  10794  sstskm  10802  supsrlem  11071  infm3  12153  nnunb  12479  nnwos  12918  fz1sbc  13607  cotr2g  14991  caubnd  15388  rpnnen2lem12  16259  isprm2  16718  pgpfac1  20124  pgpfac  20128  nrhmzr  20589  lidldvgen  21406  iunocv  21735  ismhp3  22209  istopg  22957  dfconn2  23481  1stccn  23525  iskgen3  23611  fbfinnfr  23903  iscmet3  25357  wilthlem3  27136  eqcuts2  27881  elons2  28353  onsfi  28451  isch3  31446  choc0  31531  pjnormssi  32373  reuxfrdf  32692  rabsspr  32702  rabsstp  32703  inpr0  32733  ssiun3  32760  ssdifidlprm  33647  fmcncfil  34230  bnj115  35023  bnj946  35072  bnj1211  35094  bnj1294  35114  bnj1385  35129  bnj110  35155  bnj611  35215  bnj864  35219  bnj865  35220  bnj1000  35238  bnj978  35246  bnj1049  35271  bnj1090  35276  bnj1133  35286  bnj1176  35302  bnj1186  35304  bnj1253  35314  bnj1388  35330  axprALT2  35409  axregs  35439  onvf1odlem4  35453  untuni  36064  dfon2lem8  36143  wzel  36177  dfrdg4  36306  ixpeq12dv  36581  cbvralvw2  36591  onsuct0  36806  axtco  36836  axtco1g  36841  regsfromregtco  36903  mh-infprim2bi  36912  mh-infprim3bi  36913  bj-ralvw  37369  bj-rcleqf  37515  bj-rep  37563  bj-axseprep  37564  bj-axreprepsep  37565  exrecfnlem  37878  fvineqsneq  37911  poimirlem25  38149  poimirlem30  38154  mptbi12f  38670  ralmo  38864  ralrmo3  38868  pmapglbx  40398  cdlemefrs29bpre0  41025  sn-axrep5v  42841  dford4  43611  unielss  43800  orddif0suc  43850  cllem0  44147  elmapintrab  44157  elintima  44234  ss2iundf  44240  ntrneiiso  44672  ntrneik2  44673  ntrneix2  44674  ntrneikb  44675  scottabf  44821  expandral  44871  ismnushort  44882  ralbidar  45025  rexbidar  45026  ssralv2  45112  en3lpVD  45425  ssralv2VD  45446  trintALTVD  45460  traxext  45558  dfac5prim  45571  permac8prim  45595  nregmodel  45598  ssrabf  45697  rabssf  45702  r19.3rzf  45741  rexrsb  47699  empty-surprise  50408  alsconv  50416