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 47870 or ralndv2 47871, 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 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2142	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1567	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 209	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is used 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  3339  sbralie  3341  sbralieOLD  3343  raleqf  3344  cbvralf  3348  rgen2a  3359  nfrald  3360  ralcom2  3365  rabbi  3445  rabid2f  3446  rabid2im  3447  ralv  3480  ceqsralt  3488  rspct  3566  rspc  3568  rspcimdv  3570  rspc2gv  3590  ralxpxfr2d  3604  ralab  3655  ralab2  3659  ralrab2  3660  reu2  3687  reu6  3688  reu3  3689  rmo4  3692  reu8  3695  rmo3f  3696  rmoim  3702  2reuswap  3708  2reuswap2  3709  2reu5lem2  3718  2reu5lem3  3719  2rmoswap  3723  rmo2  3839  rmo3  3841  rmoanim  3847  cbvralcsf  3894  dfss3  3925  dfss3f  3928  ssralv  4005  ralss  4009  ssabral  4017  ss2rab  4022  rabss  4023  ssrab  4024  ss2rabd  4025  dfdif3OLD  4072  rexdifi  4103  ralunb  4149  reuss2  4278  rspn0  4310  n0el  4318  disj  4409  disj1  4411  rzal  4454  ralf0  4457  r19.2z  4459  r19.3rz  4461  falseral0OLD  4475  ralidmw  4476  ralidm  4477  rabsssn  4633  ralsnsg  4635  ralsng  4640  unissb  4905  dfint2  4913  elint2  4918  elintrab  4924  ssintrab  4935  dfiin2g  4994  invdisj  5094  disjss3  5107  dftr5  5221  zfrep6  5249  reusv2lem4  5371  axprlem2  5394  axprlem4OLD  5400  axprlem5OLD  5401  dffr6  5616  raliunxp  5824  dmopab3  5908  rnopab3  5945  asymref  6115  asymref2  6116  dfpo2  6297  dffun7  6563  funcnv  6605  fnres  6662  mptfnf  6670  fnopabg  6672  dff3  7095  dffo3  7097  dffo3f  7101  fnssintima  7362  imaeqalov  7651  find  7890  funcnvuni  7927  zfrep6OLD  7950  ralxp3f  8131  frpoins3xpg  8134  frpoins3xp3g  8135  nfixpw  8912  nfixp  8913  marypha2lem3  9395  zfregcl  9554  zfregclOLD  9555  zfinf2  9609  scottabf  9866  scottexsOLD  9870  scott0bsOLD  9872  aceq1  10108  aceq2  10110  kmlem12  10152  kmlem14  10154  kmlem15  10155  zorn2lem4  10489  zorn2lem5  10490  axgroth5  10815  grothprim  10825  sstskm  10833  supsrlem  11102  infm3  12180  nnunb  12506  nnwos  12945  fz1sbc  13635  cotr2g  15020  caubnd  15417  rpnnen2lem12  16287  isprm2  16746  pgpfac1  20158  pgpfac  20162  nrhmzr  20647  ssdifidlprm  21497  lidldvgen  21513  iunocv  21842  ismhp3  22316  istopg  23063  dfconn2  23587  1stccn  23631  iskgen3  23717  fbfinnfr  24009  iscmet3  25463  wilthlem3  27245  eqcuts2  27990  elons2  28462  onsfi  28560  isch3  31604  choc0  31689  pjnormssi  32531  reuxfrdf  32848  rabsspr  32858  rabsstp  32859  inpr0  32889  ssiun3  32914  fmcncfil  34330  bnj115  35123  bnj946  35172  bnj1211  35194  bnj1294  35214  bnj1385  35229  bnj110  35255  bnj611  35315  bnj864  35319  bnj865  35320  bnj1000  35338  bnj978  35346  bnj1049  35371  bnj1090  35376  bnj1133  35386  bnj1176  35402  bnj1186  35404  bnj1253  35414  bnj1388  35430  axprALT2  35512  axregs  35560  onvf1odlem4  35598  untuni  36209  dfon2lem8  36288  wzel  36322  dfrdg4  36451  ixpeq12dv  36756  cbvralvw2  36766  onsuct0  36980  axtco  37010  axtco1g  37015  regsfromregtco  37077  mh-infprim2bi  37086  mh-infprim3bi  37087  bj-ralvw  37542  bj-rcleqf  37689  bj-rep  37738  bj-axseprep  37739  bj-axreprepsep  37740  exrecfnlem  38053  fvineqsneq  38086  poimirlem25  38324  poimirlem30  38329  mptbi12f  38843  ralmo  39037  ralrmo3  39041  pmapglbx  40571  cdlemefrs29bpre0  41198  sn-axrep5v  43016  dford4  43784  unielss  43973  orddif0suc  44023  cllem0  44320  elmapintrab  44330  elintima  44407  ss2iundf  44413  ntrneiiso  44845  ntrneik2  44846  ntrneix2  44847  ntrneikb  44848  expandral  45028  ismnushort  45039  ralbidar  45182  rexbidar  45183  ssralv2  45268  en3lpVD  45581  ssralv2VD  45602  trintALTVD  45616  traxext  45714  dfac5prim  45727  permac8prim  45751  nregmodel  45754  ssrabf  45860  rabssf  45865  r19.3rzf  45904  rexrsb  47865  empty-surprise  50588  dfrals2  50596  alsralrex  50618  dfralseu2  50629