Definition df-ral 3062

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 44618 or ralndv2 44619, 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 1537	. . . . 5 class 𝑥
6	5, 3	wcel 2103	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1536	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 205	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3063  raln  3069  alral  3075  ralimi2  3077  ral2imi  3084  ralbii2  3088  ralrexbidOLD  3106  r19.26m  3109  hbralrimi  3133  ralimdv2  3145  ralbidv2  3148  r19.21vOLD  3152  r2allem  3155  r3al  3157  rspw  3168  rsp  3169  r19.21t  3177  ralrimd  3181  nfra1  3182  hbral  3184  nfraldw  3186  nfraldwOLD  3187  nfrald  3188  nfra2wOLD  3193  rgen2a  3196  ralbidaOLD  3198  ralcom4  3202  ralcom4OLD  3203  r19.23t  3256  ralcom2  3290  rabid2f  3312  rabid2OLD  3314  rabbi  3315  raleqf  3331  raleqbidvv  3337  moel  3357  moelOLD  3358  cbvralfw  3367  cbvralfwOLD  3368  cbvralf  3370  cbvralvw  3382  cbvraldva2  3391  ralv  3455  ceqsralt  3462  rspct  3546  rspc  3548  rspcimdv  3550  rspc2gv  3568  ralxpxfr2d  3575  ralab  3627  ralabOLD  3628  ralab2  3633  ralrab2  3634  reu2  3659  reu6  3660  reu3  3661  rmo4  3664  reu8  3667  rmo3f  3668  rmoim  3674  2reuswap  3680  2reuswap2  3681  2reu5lem2  3690  2reu5lem3  3691  2rmoswap  3695  rmo2  3819  rmo3  3821  rmoanim  3826  cbvralcsf  3876  dfss3  3908  dfss3f  3911  ssabral  3995  ss2rab  4003  rabss  4004  ssrab  4005  dfdif3  4048  rexdifi  4079  ralunb  4124  reuss2  4248  rspn0  4285  n0el  4294  disj  4380  disjOLD  4381  disj1  4383  r19.2z  4424  r19.3rz  4426  ralidmw  4437  rzal  4438  ralidm  4441  ralf0  4443  ralidmOLD  4445  ralf0OLD  4447  falseral0  4449  rabsssn  4602  ralsnsg  4603  ralsng  4608  unissb  4872  dfint2  4880  elint2  4885  elintrab  4890  ssintrab  4901  dfiin2g  4961  invdisj  5057  disjss3  5072  dftr5  5193  reusv2lem4  5323  axprlem2  5346  axprlem4  5348  axprlem5  5349  dffr6  5546  raliunxp  5749  dmopab3  5829  asymref  6024  asymref2  6025  dfpo2  6201  dffun7  6466  funcnv  6508  fnres  6566  mptfnf  6575  fnopabg  6577  dff3  6983  dffo3  6985  find  7750  findOLD  7751  funcnvuni  7785  zfrep6  7804  nfixpw  8711  nfixp  8712  marypha2lem3  9203  zfregcl  9360  zfinf2  9407  scottexs  9652  scott0s  9653  aceq1  9880  aceq2  9882  kmlem12  9924  kmlem14  9926  kmlem15  9927  zorn2lem4  10262  zorn2lem5  10263  ingru  10578  axgroth5  10587  grothprim  10597  sstskm  10605  supsrlem  10874  infm3  11941  nnunb  12236  nnwos  12662  fz1sbc  13339  cotr2g  14694  caubnd  15077  rpnnen2lem12  15941  isprm2  16394  pgpfac1  19690  pgpfac  19694  lidldvgen  20533  iunocv  20893  ismhp3  21340  istopg  22051  dfconn2  22577  1stccn  22621  iskgen3  22707  fbfinnfr  22999  iscmet3  24464  wilthlem3  26226  isch3  29610  choc0  29695  pjnormssi  30537  nelbOLDOLD  30824  reuxfrdf  30846  inpr0  30887  ssiun3  30905  fmcncfil  31888  bnj115  32711  bnj946  32761  bnj1142  32776  bnj1211  32784  bnj1294  32804  bnj1385  32819  bnj110  32845  bnj611  32905  bnj864  32909  bnj865  32910  bnj1000  32928  bnj978  32936  bnj1049  32961  bnj1090  32966  bnj1133  32976  bnj1176  32992  bnj1186  32994  bnj1253  33004  bnj1388  33020  untuni  33657  fnssintima  33683  ralxp3f  33692  dfon2lem8  33773  frpoins3xpg  33794  frpoins3xp3g  33795  wzel  33825  eqscut2  34007  dfrdg4  34260  onsuct0  34637  bj-ralvw  35071  bj-rcleqf  35222  exrecfnlem  35557  fvineqsneq  35590  poimirlem25  35809  poimirlem30  35814  nninfnub  35916  mptbi12f  36331  pmapglbx  37788  cdlemefrs29bpre0  38415  sn-axrep5v  40190  dford4  40856  cllem0  41178  elmapintrab  41189  elintima  41266  ss2iundf  41272  ntrneiiso  41706  ntrneik2  41707  ntrneix2  41708  ntrneikb  41709  scottabf  41863  expandral  41913  ismnushort  41924  ralbidar  42068  rexbidar  42069  ssralv2  42156  en3lpVD  42470  ssralv2VD  42491  trintALTVD  42505  ssrabf  42669  rabssf  42673  dffo3f  42728  rexrsb  44613  nrhmzr  45452  empty-surprise  46507  alsconv  46515