Definition df-ral 3049

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 47229 or ralndv2 47230, 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 3048	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1539	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3050  raln  3056  alral  3062  ralimi2  3065  ral2imi  3072  ralbii2  3075  r19.26m  3092  r2allem  3121  hbralrimi  3123  ralimdv2  3142  ralbidv2  3152  r3al  3171  rspw  3210  cbvralvw  3211  rsp  3221  r19.21t  3227  r19.23t  3229  ralrimd  3238  nfra1  3257  ralcom4  3259  cbvralfw  3273  hbral  3277  nfraldw  3278  cbvralsvw  3284  raleqbidvvOLD  3302  cbvraldva2  3315  sbralie  3319  sbralieOLD  3321  raleqf  3322  cbvralf  3327  rgen2a  3338  nfrald  3339  ralcom2  3344  rabbi  3426  rabid2f  3427  rabid2im  3428  ralv  3464  ceqsralt  3472  rspct  3559  rspc  3561  rspcimdv  3563  rspc2gv  3583  ralxpxfr2d  3597  ralab  3648  ralab2  3652  ralrab2  3653  reu2  3680  reu6  3681  reu3  3682  rmo4  3685  reu8  3688  rmo3f  3689  rmoim  3695  2reuswap  3701  2reuswap2  3702  2reu5lem2  3711  2reu5lem3  3712  2rmoswap  3716  rmo2  3834  rmo3  3836  rmoanim  3841  cbvralcsf  3888  dfss3  3919  dfss3f  3922  ssralv  3999  ralss  4005  ssabral  4013  ss2rab  4018  rabss  4019  ssrab  4020  ss2rabd  4021  dfdif3OLD  4067  rexdifi  4099  ralunb  4146  reuss2  4275  rspn0  4305  n0el  4313  disj  4399  disj1  4401  r19.2z  4444  r19.3rz  4446  ralidmw  4457  rzal  4458  ralidm  4461  ralf0  4463  falseral0  4465  rabsssn  4620  ralsnsg  4622  ralsng  4627  unissb  4891  dfint2  4899  elint2  4904  elintrab  4910  ssintrab  4921  dfiin2g  4981  invdisj  5079  disjss3  5092  dftr5  5204  reusv2lem4  5341  axprlem2  5364  axprlem4  5366  axprlem4OLD  5369  axprlem5OLD  5370  dffr6  5575  raliunxp  5783  dmopab3  5863  rnopab3  5900  asymref  6067  asymref2  6068  dfpo2  6248  dffun7  6513  funcnv  6555  fnres  6613  mptfnf  6621  fnopabg  6623  dff3  7039  dffo3  7041  dffo3f  7045  fnssintima  7302  imaeqalov  7591  find  7831  funcnvuni  7868  zfrep6  7893  ralxp3f  8073  frpoins3xpg  8076  frpoins3xp3g  8077  nfixpw  8846  nfixp  8847  marypha2lem3  9328  zfregcl  9487  zfregclOLD  9488  zfinf2  9539  scottexs  9787  scott0s  9788  aceq1  10015  aceq2  10017  kmlem12  10060  kmlem14  10062  kmlem15  10063  zorn2lem4  10397  zorn2lem5  10398  ingru  10713  axgroth5  10722  grothprim  10732  sstskm  10740  supsrlem  11009  infm3  12088  nnunb  12384  nnwos  12815  fz1sbc  13502  cotr2g  14885  caubnd  15268  rpnnen2lem12  16136  isprm2  16595  pgpfac1  19996  pgpfac  20000  nrhmzr  20454  lidldvgen  21273  iunocv  21620  ismhp3  22058  istopg  22811  dfconn2  23335  1stccn  23379  iskgen3  23465  fbfinnfr  23757  iscmet3  25221  wilthlem3  27008  eqscut2  27748  elons2  28196  onsfi  28284  isch3  31223  choc0  31308  pjnormssi  32150  reuxfrdf  32472  rabsspr  32483  rabsstp  32484  inpr0  32514  ssiun3  32540  ssdifidlprm  33430  fmcncfil  33965  bnj115  34758  bnj946  34807  bnj1142  34822  bnj1211  34830  bnj1294  34850  bnj1385  34865  bnj110  34891  bnj611  34951  bnj864  34955  bnj865  34956  bnj1000  34974  bnj978  34982  bnj1049  35007  bnj1090  35012  bnj1133  35022  bnj1176  35038  bnj1186  35040  bnj1253  35050  bnj1388  35066  r1omhfb  35144  r1omhfbregs  35154  axregs  35166  onvf1odlem4  35171  untuni  35774  dfon2lem8  35853  wzel  35887  dfrdg4  36016  ixpeq12dv  36281  cbvralvw2  36291  onsuct0  36506  bj-ralvw  36944  bj-rcleqf  37090  exrecfnlem  37444  fvineqsneq  37477  poimirlem25  37705  poimirlem30  37710  nninfnub  37811  mptbi12f  38226  eqab2  38305  pmapglbx  39888  cdlemefrs29bpre0  40515  sn-axrep5v  42334  dford4  43146  unielss  43335  orddif0suc  43385  cllem0  43683  elmapintrab  43693  elintima  43770  ss2iundf  43776  ntrneiiso  44208  ntrneik2  44209  ntrneix2  44210  ntrneikb  44211  scottabf  44357  expandral  44407  ismnushort  44418  ralbidar  44561  rexbidar  44562  ssralv2  44648  en3lpVD  44961  ssralv2VD  44982  trintALTVD  44996  traxext  45094  dfac5prim  45107  permac8prim  45131  nregmodel  45134  ssrabf  45235  rabssf  45240  r19.3rzf  45279  rexrsb  47224  empty-surprise  49907  alsconv  49915