Definition df-ral 3066

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 44269 or ralndv2 44270, 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 3061	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1542	. . . . 5 class 𝑥
6	5, 3	wcel 2110	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1541	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 209	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3071  alral  3077  raln  3078  ral2imi  3079  ralimi2  3080  ralbii2  3086  r19.26m  3095  r19.21v  3098  ralimdv2  3099  hbralrimi  3103  ralbidv2  3116  r2allem  3121  r3al  3123  rspw  3126  rsp  3127  r19.21t  3135  ralrimd  3139  nfra1  3140  hbral  3142  nfraldw  3144  nfraldwOLD  3145  nfrald  3146  nfra2w  3149  rgen2a  3152  ralbida  3153  ralcom4  3157  r19.23t  3232  ralrexbid  3241  ralcom2  3275  rabid2  3293  rabid2f  3294  rabbi  3295  raleqf  3309  raleqbidvv  3315  moel  3335  cbvralfw  3344  cbvralfwOLD  3345  cbvralf  3347  cbvralvw  3358  cbvraldva2  3367  ralv  3432  ceqsralt  3439  rspct  3523  rspc  3525  rspcimdv  3527  rspc2gv  3546  ralxpxfr2d  3553  ralab  3606  ralab2  3610  ralab2OLD  3611  ralrab2  3612  reu2  3638  reu6  3639  reu3  3640  rmo4  3643  reu8  3646  rmo3f  3647  rmoim  3653  2reuswap  3659  2reuswap2  3660  2reu5lem2  3669  2reu5lem3  3670  2rmoswap  3674  rmo2  3799  rmo3  3801  rmoanim  3806  cbvralcsf  3856  dfss3  3888  dfss3f  3891  ssabral  3976  ss2rab  3984  rabss  3985  ssrab  3986  dfdif3  4029  rexdifi  4060  ralunb  4105  reuss2  4230  rspn0  4267  n0el  4276  disj  4362  disjOLD  4363  disj1  4365  r19.2z  4406  r19.3rz  4408  ralidmw  4419  rzal  4420  ralidm  4423  ralf0  4425  ralidmOLD  4427  ralf0OLD  4429  falseral0  4431  rabsssn  4583  ralsnsg  4584  ralsng  4589  unissb  4853  dfint2  4861  elint2  4866  elintrab  4871  ssintrab  4882  dfiin2g  4941  invdisj  5037  disjss3  5052  dftr5  5164  reusv2lem4  5294  axprlem2  5317  axprlem4  5319  axprlem5  5320  raliunxp  5708  dmopab3  5788  asymref  5981  asymref2  5982  dffun7  6407  funcnv  6449  fnres  6504  mptfnf  6513  fnopabg  6515  dff3  6919  dffo3  6921  find  7674  findOLD  7675  funcnvuni  7709  zfrep6  7728  nfixpw  8597  nfixp  8598  marypha2lem3  9053  zfregcl  9210  zfinf2  9257  scottexs  9503  scott0s  9504  aceq1  9731  aceq2  9733  kmlem12  9775  kmlem14  9777  kmlem15  9778  zorn2lem4  10113  zorn2lem5  10114  ingru  10429  axgroth5  10438  grothprim  10448  sstskm  10456  supsrlem  10725  infm3  11791  nnunb  12086  nnwos  12511  fz1sbc  13188  cotr2g  14539  caubnd  14922  rpnnen2lem12  15786  isprm2  16239  pgpfac1  19467  pgpfac  19471  lidldvgen  20293  iunocv  20643  ismhp3  21083  istopg  21792  dfconn2  22316  1stccn  22360  iskgen3  22446  fbfinnfr  22738  iscmet3  24190  wilthlem3  25952  isch3  29322  choc0  29407  pjnormssi  30249  nelbOLD  30536  reuxfrdf  30558  inpr0  30599  ssiun3  30617  fmcncfil  31595  bnj115  32416  bnj946  32467  bnj1142  32482  bnj1211  32490  bnj1294  32510  bnj1385  32525  bnj110  32551  bnj611  32611  bnj864  32615  bnj865  32616  bnj1000  32634  bnj978  32642  bnj1049  32667  bnj1090  32672  bnj1133  32682  bnj1176  32698  bnj1186  32700  bnj1253  32710  bnj1388  32726  untuni  33363  fnssintima  33391  ralxp3f  33401  dfpo2  33441  dfon2lem8  33485  frpoins3xpg  33524  frpoins3xp3g  33525  wzel  33555  eqscut2  33737  dfrdg4  33990  onsuct0  34367  bj-ralvw  34801  bj-rcleqf  34952  exrecfnlem  35287  fvineqsneq  35320  poimirlem25  35539  poimirlem30  35544  nninfnub  35646  mptbi12f  36061  pmapglbx  37520  cdlemefrs29bpre0  38147  sn-axrep5v  39907  dford4  40554  cllem0  40849  elmapintrab  40860  elintima  40938  ss2iundf  40944  ntrneiiso  41378  ntrneik2  41379  ntrneix2  41380  ntrneikb  41381  scottabf  41531  expandral  41581  ismnushort  41592  ralbidar  41736  rexbidar  41737  ssralv2  41824  en3lpVD  42138  ssralv2VD  42159  trintALTVD  42173  ssrabf  42337  rabssf  42341  dffo3f  42390  rexrsb  44264  nrhmzr  45104  empty-surprise  46157  alsconv  46165