Definition df-ral 3110

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 42847 or ralndv2 42848, 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 3105	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1521	. . . . 5 class 𝑥
6	5, 3	wcel 2081	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1520	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 207	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3115  alral  3121  raln  3122  ral2imi  3123  ralimi2  3124  ralbii2  3130  ralanidOLD  3136  r19.26m  3140  r19.21v  3142  ralimdv2  3143  hbralrimi  3147  ralbidv2  3162  r2allem  3167  r3al  3169  rsp  3172  r19.21t  3181  ralrimd  3185  nfra1  3186  hbral  3188  nfrald  3190  rgen2a  3193  ralbida  3194  ralcom4  3199  r19.23t  3274  ralrexbid  3283  ralcom2  3324  rabid2  3340  rabid2f  3341  rabbi  3342  raleqf  3357  cbvralf  3397  cbvraldva2  3407  ralv  3462  ceqsralt  3471  rspct  3551  rspc  3553  rspcimdv  3560  rspc2gv  3571  ralxpxfr2d  3578  ralab  3623  ralab2  3627  ralab2OLD  3628  ralrab2  3629  reu2  3653  reu6  3654  reu3  3655  rmo4  3658  reu8  3661  rmo3f  3662  rmoim  3668  2reuswap  3674  2reuswap2  3675  2reu5lem2  3684  2reu5lem3  3685  2rmoswap  3689  rmo2  3802  rmo3  3804  rmo3OLD  3805  rmoanim  3810  cbvralcsf  3853  dfss3  3882  dfss3f  3885  ssabral  3967  ss2rab  3972  rabss  3973  ssrab  3974  dfdif3  4016  rexdifi  4047  ralunb  4092  reuss2  4207  n0el  4245  disj  4317  disj1  4319  r19.2z  4358  r19.3rz  4360  ralidm  4373  ralf0  4375  falseral0  4377  rabsssn  4516  ralsnsg  4517  unissb  4780  dfint2  4788  elint2  4793  elintrab  4798  ssintrab  4809  dfiin2g  4864  invdisj  4952  disjss3  4965  dftr5  5071  reusv2lem4  5198  axprlem2  5221  axprlem4  5223  axprlem5  5224  raliunxp  5601  dmopab3  5679  asymref  5857  asymref2  5858  dffun7  6257  funcnv  6298  fnres  6349  mptfnf  6356  fnopabg  6358  dff3  6734  dffo3  6736  find  7468  funcnvuni  7497  zfrep6  7517  nfixp  8334  marypha2lem3  8752  zfregcl  8909  zfinf2  8956  scottexs  9167  scott0s  9168  aceq1  9394  aceq2  9396  kmlem12  9438  kmlem14  9440  kmlem15  9441  zorn2lem4  9772  zorn2lem5  9773  ingru  10088  axgroth5  10097  grothprim  10107  sstskm  10115  supsrlem  10384  infm3  11453  nnunb  11746  nnwos  12169  fz1sbc  12838  cotr2g  14175  caubnd  14557  rpnnen2lem12  15416  isprm2  15860  pgpfac1  18924  pgpfac  18928  lidldvgen  19722  iunocv  20512  istopg  21192  dfconn2  21716  1stccn  21760  iskgen3  21846  fbfinnfr  22138  iscmet3  23584  wilthlem3  25334  isch3  28714  choc0  28799  pjnormssi  29641  nelb  29929  moel  29949  reuxfrdf  29952  inpr0  29986  ssiun3  30005  fmcncfil  30796  bnj115  31617  bnj946  31668  bnj1142  31683  bnj1211  31691  bnj1294  31711  bnj1385  31726  bnj110  31751  bnj611  31811  bnj864  31815  bnj865  31816  bnj1000  31834  bnj978  31842  bnj1049  31865  bnj1090  31870  bnj1133  31880  bnj1176  31896  bnj1186  31898  bnj1253  31908  bnj1388  31924  untuni  32550  dfpo2  32606  dfon2lem8  32650  wzel  32727  dfrdg4  33028  onsuct0  33405  bj-ralvw  33778  exrecfnlem  34217  fvineqsneq  34250  poimirlem25  34474  poimirlem30  34479  nninfnub  34584  mptbi12f  35002  pmapglbx  36462  cdlemefrs29bpre0  37089  sn-axrep5v  38664  dford4  39137  cllem0  39436  elmapintrab  39447  elintima  39509  ss2iundf  39515  ntrneiiso  39952  ntrneik2  39953  ntrneix2  39954  ntrneikb  39955  scottabf  40099  expandral  40149  ralbidar  40342  rexbidar  40343  ssralv2  40430  en3lpVD  40744  ssralv2VD  40765  trintALTVD  40779  ssrabf  40947  rabssf  40951  dffo3f  41004  rexrsb  42841  nrhmzr  43649  empty-surprise  44390  alsconv  44398