Definition df-ral 3045

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 47090 or ralndv2 47091, 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 3044	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1538	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3046  raln  3052  alral  3058  ralimi2  3061  ral2imi  3068  ralbii2  3071  r19.26m  3088  r2allem  3117  hbralrimi  3119  ralimdv2  3138  ralbidv2  3148  r3al  3167  rspw  3206  cbvralvw  3207  rsp  3217  r19.21t  3223  r19.23t  3225  ralrimd  3234  nfra1  3253  ralcom4  3255  cbvralfw  3270  hbral  3274  nfraldw  3275  cbvralsvw  3281  raleqbidvvOLD  3299  cbvraldva2  3312  sbralie  3317  sbralieOLD  3319  raleqf  3320  cbvralf  3325  rgen2a  3336  nfrald  3337  ralcom2  3342  rabbi  3427  rabid2f  3428  rabid2im  3429  ralv  3465  ceqsralt  3473  rspct  3565  rspc  3567  rspcimdv  3569  rspc2gv  3589  ralxpxfr2d  3603  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  3841  rmo3  3843  rmoanim  3848  cbvralcsf  3895  dfss3  3926  dfss3f  3929  ssralv  4006  ralss  4012  ssabral  4019  ss2rab  4024  rabss  4025  ssrab  4026  dfdif3OLD  4071  rexdifi  4103  ralunb  4150  reuss2  4279  rspn0  4309  n0el  4317  disj  4403  disj1  4405  r19.2z  4448  r19.3rz  4450  ralidmw  4461  rzal  4462  ralidm  4465  ralf0  4467  falseral0  4469  rabsssn  4622  ralsnsg  4624  ralsng  4629  unissb  4893  dfint2  4901  elint2  4906  elintrab  4913  ssintrab  4924  dfiin2g  4984  invdisj  5081  disjss3  5094  dftr5  5206  reusv2lem4  5343  axprlem2  5366  axprlem4  5368  axprlem4OLD  5371  axprlem5OLD  5372  dffr6  5579  raliunxp  5786  dmopab3  5866  rnopab3  5902  asymref  6069  asymref2  6070  dfpo2  6248  dffun7  6513  funcnv  6555  fnres  6613  mptfnf  6621  fnopabg  6623  dff3  7038  dffo3  7040  dffo3f  7044  fnssintima  7303  imaeqalov  7592  find  7835  funcnvuni  7872  zfrep6  7897  ralxp3f  8077  frpoins3xpg  8080  frpoins3xp3g  8081  nfixpw  8850  nfixp  8851  marypha2lem3  9346  zfregcl  9505  zfregclOLD  9506  zfinf2  9557  scottexs  9802  scott0s  9803  aceq1  10030  aceq2  10032  kmlem12  10075  kmlem14  10077  kmlem15  10078  zorn2lem4  10412  zorn2lem5  10413  ingru  10728  axgroth5  10737  grothprim  10747  sstskm  10755  supsrlem  11024  infm3  12102  nnunb  12398  nnwos  12834  fz1sbc  13521  cotr2g  14901  caubnd  15284  rpnnen2lem12  16152  isprm2  16611  pgpfac1  19979  pgpfac  19983  nrhmzr  20440  lidldvgen  21259  iunocv  21606  ismhp3  22045  istopg  22798  dfconn2  23322  1stccn  23366  iskgen3  23452  fbfinnfr  23744  iscmet3  25209  wilthlem3  26996  eqscut2  27735  elons2  28182  onsfi  28270  isch3  31203  choc0  31288  pjnormssi  32130  reuxfrdf  32453  rabsspr  32463  rabsstp  32464  inpr0  32494  ssiun3  32520  ssdifidlprm  33405  fmcncfil  33897  bnj115  34691  bnj946  34740  bnj1142  34755  bnj1211  34763  bnj1294  34783  bnj1385  34798  bnj110  34824  bnj611  34884  bnj864  34888  bnj865  34889  bnj1000  34907  bnj978  34915  bnj1049  34940  bnj1090  34945  bnj1133  34955  bnj1176  34971  bnj1186  34973  bnj1253  34983  bnj1388  34999  axregs  35073  onvf1odlem4  35078  untuni  35681  dfon2lem8  35763  wzel  35797  dfrdg4  35924  ixpeq12dv  36189  cbvralvw2  36199  onsuct0  36414  bj-ralvw  36852  bj-rcleqf  36998  exrecfnlem  37352  fvineqsneq  37385  poimirlem25  37624  poimirlem30  37629  nninfnub  37730  mptbi12f  38145  eqab2  38222  pmapglbx  39748  cdlemefrs29bpre0  40375  sn-axrep5v  42189  dford4  43002  unielss  43191  orddif0suc  43241  cllem0  43539  elmapintrab  43549  elintima  43626  ss2iundf  43632  ntrneiiso  44064  ntrneik2  44065  ntrneix2  44066  ntrneikb  44067  scottabf  44213  expandral  44263  ismnushort  44274  ralbidar  44418  rexbidar  44419  ssralv2  44505  en3lpVD  44818  ssralv2VD  44839  trintALTVD  44853  traxext  44951  dfac5prim  44964  permac8prim  44988  nregmodel  44991  ssrabf  45092  rabssf  45097  r19.3rzf  45136  rexrsb  47085  empty-surprise  49768  alsconv  49776