Definition df-ral 3081

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 48379 or ralndv2 48380, 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 3080	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2147	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1568	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 209	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is used by:  rgen  3082  ralrid  3088  raln  3089  ralimi2  3098  ral2imi  3105  ralbii2  3108  r19.26m  3125  r2allem  3154  ralimdv2  3175  ralbidv2  3185  r3al  3204  rspw  3243  cbvralvw  3244  rsp  3254  r19.21t  3260  r19.23t  3262  ralrimd  3271  nfra1  3290  ralcom4  3292  cbvralfw  3306  hbral  3310  nfraldw  3311  cbvralsvw  3317  cbvraldva2  3340  sbralie  3342  sbralieOLD  3344  raleqf  3345  cbvralf  3349  rgen2a  3360  nfrald  3361  ralcom2  3366  rabbi  3445  rabid2f  3446  rabid2im  3447  ralv  3480  ceqsralt  3488  rspct  3566  rspc  3568  rspcimdv  3570  rspc2gv  3589  ralxpxfr2d  3603  ralab  3654  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  3838  rmo3  3840  rmoanim  3846  cbvralcsf  3893  dfss3  3902  dfss3f  3905  ssralv  3982  ralss  3986  ssabral  3992  ss2rab  3997  rabss  3998  ssrab  3999  ss2rabd  4000  rexdifi  4089  ralunb  4198  reuss2  4274  rspn0  4307  n0el  4315  disj  4406  disj1  4408  rzal  4453  ralf0  4456  r19.2z  4458  r19.3rz  4460  falseral0OLD  4474  ralidmw  4475  ralidm  4476  rabsssn  4629  ralsnsg  4631  ralsng  4636  unissb  4904  dfint2  4912  elint2  4917  elintrab  4923  ssintrab  4934  dfiin2g  4992  invdisj  5092  disjss3  5105  dftr5  5219  zfrep6  5245  reusv2lem4  5367  axprlem2  5390  dffr6  5611  raliunxp  5821  dmopab3  5907  rnopab3  5944  asymref  6121  asymref2  6122  dfpo2  6314  dffun7  6584  funcnv  6628  fnres  6685  mptfnf  6693  fnopabg  6695  dff3  7121  dffo3  7123  dffo3f  7127  fnssintima  7392  imaeqalov  7681  find  7928  funcnvuni  7965  zfrep6OLD  7988  ralxp3f  8178  frpoins3xpg  8181  frpoins3xp3g  8182  nfixpw  8969  nfixp  8970  marypha2lem3  9453  zfregcl  9612  zfregclOLD  9613  zfinf2  9667  scottabf  9963  scottexsOLD  9967  scott0bsOLD  9969  aceq1  10220  aceq2  10222  kmlem12  10264  kmlem14  10266  kmlem15  10267  zorn2lem4  10601  zorn2lem5  10602  axgroth5  10933  grothprim  10943  sstskm  10951  supsrlem  11220  infm3  12300  nnunb  12626  nnwos  13066  fz1sbc  13758  cotr2g  15155  caubnd  15552  rpnnen2lem12  16419  isprm2  16883  pgpfac1  20323  pgpfac  20327  nrhmzr  20816  ssdifidlprm  21669  lidldvgen  21685  iunocv  22014  ismhp3  22490  istopg  23240  dfconn2  23764  1stccn  23809  iskgen3  23895  fbfinnfr  24187  iscmet3  25641  wilthlem3  27424  eqcuts2  28199  elons2  28671  onsfi  28769  isch3  31870  choc0  31955  pjnormssi  32797  reuxfrdf  33156  rabsspr  33166  rabsstp  33167  inpr0  33197  ssiun3  33222  fmcncfil  34630  bnj115  35423  bnj946  35472  bnj1211  35494  bnj1294  35514  bnj1385  35529  bnj110  35555  bnj611  35615  bnj864  35619  bnj865  35620  bnj1000  35638  bnj978  35646  bnj1049  35671  bnj1090  35676  bnj1133  35686  bnj1176  35702  bnj1186  35704  bnj1253  35714  bnj1388  35730  reu6f  35776  axprALT2  35815  axregs  35906  onvf1odlem4  36033  onprcf1acwevdlem1  36044  mirimanofffr  36628  untuni  36651  dfon2lem8  36729  wzel  36763  dfrdg4  36892  ixpeq12dv  37182  cbvralvw2  37192  onsuct0  37406  axtco  37436  axtco1g  37441  regsfromregtco  37503  mh-infprim2bi  37512  mh-infprim3bi  37513  bj-ralvw  37968  bj-rcleqf  38115  bj-rep  38179  bj-axseprep  38180  bj-axreprepsep  38181  exrecfnlem  38493  fvineqsneq  38526  poimirlem25  38754  poimirlem30  38759  mptbi12f  39289  ralmo  39483  ralrmo3  39487  pmapglbx  41017  cdlemefrs29bpre0  41644  sn-axrep5v  43462  dford4  44227  unielss  44410  orddif0suc  44460  cllem0  44757  elmapintrab  44767  elintima  44843  ss2iundf  44849  ntrneiiso  45281  ntrneik2  45282  ntrneix2  45283  ntrneikb  45284  expandral  45464  ismnushort  45475  ralbidar  45617  rexbidar  45618  ssralv2  45703  en3lpVD  46016  ssralv2VD  46037  trintALTVD  46051  traxext  46160  dfac5prim  46173  permac8prim  46197  nregmodel  46200  ssrabf  46332  rabssf  46337  r19.3rzf  46376  rexrsb  48374  empty-surprise  51156  dfrals2  51164  alsralrex  51186  dfralseu2  51197