Definition df-ral 3053

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 47494 or ralndv2 47495, 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 3052	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1540	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3054  ralrid  3060  raln  3061  ralimi2  3070  ral2imi  3077  ralbii2  3080  r19.26m  3097  r2allem  3126  ralimdv2  3147  ralbidv2  3157  r3al  3176  rspw  3215  cbvralvw  3216  rsp  3226  r19.21t  3232  r19.23t  3234  ralrimd  3243  nfra1  3262  ralcom4  3264  cbvralfw  3278  hbral  3282  nfraldw  3283  cbvralsvw  3289  raleqbidvvOLD  3307  cbvraldva2  3320  sbralie  3324  sbralieOLD  3326  raleqf  3327  cbvralf  3332  rgen2a  3343  nfrald  3344  ralcom2  3349  rabbi  3431  rabid2f  3432  rabid2im  3433  ralv  3469  ceqsralt  3477  rspct  3564  rspc  3566  rspcimdv  3568  rspc2gv  3588  ralxpxfr2d  3602  ralab  3653  ralab2  3657  ralrab2  3658  reu2  3685  reu6  3686  reu3  3687  rmo4  3690  reu8  3693  rmo3f  3694  rmoim  3700  2reuswap  3706  2reuswap2  3707  2reu5lem2  3716  2reu5lem3  3717  2rmoswap  3721  rmo2  3839  rmo3  3841  rmoanim  3846  cbvralcsf  3893  dfss3  3924  dfss3f  3927  ssralv  4004  ralss  4010  ssabral  4018  ss2rab  4023  rabss  4024  ssrab  4025  ss2rabd  4026  dfdif3OLD  4072  rexdifi  4104  ralunb  4151  reuss2  4280  rspn0  4310  n0el  4318  disj  4404  disj1  4406  rzal  4449  ralf0  4452  r19.2z  4454  r19.3rz  4456  falseral0OLD  4470  ralidmw  4471  ralidm  4472  rabsssn  4627  ralsnsg  4629  ralsng  4634  unissb  4898  dfint2  4906  elint2  4911  elintrab  4917  ssintrab  4928  dfiin2g  4988  invdisj  5086  disjss3  5099  dftr5  5211  zfrep6  5238  reusv2lem4  5350  axprlem2  5373  axprlem4OLD  5378  axprlem5OLD  5379  dffr6  5590  raliunxp  5798  dmopab3  5878  rnopab3  5915  asymref  6083  asymref2  6084  dfpo2  6264  dffun7  6529  funcnv  6571  fnres  6629  mptfnf  6637  fnopabg  6639  dff3  7056  dffo3  7058  dffo3f  7062  fnssintima  7320  imaeqalov  7609  find  7849  funcnvuni  7886  zfrep6OLD  7911  ralxp3f  8091  frpoins3xpg  8094  frpoins3xp3g  8095  nfixpw  8868  nfixp  8869  marypha2lem3  9354  zfregcl  9513  zfregclOLD  9514  zfinf2  9565  scottexs  9813  scott0s  9814  aceq1  10041  aceq2  10043  kmlem12  10086  kmlem14  10088  kmlem15  10089  zorn2lem4  10423  zorn2lem5  10424  axgroth5  10749  grothprim  10759  sstskm  10767  supsrlem  11036  infm3  12115  nnunb  12411  nnwos  12842  fz1sbc  13530  cotr2g  14913  caubnd  15296  rpnnen2lem12  16164  isprm2  16623  pgpfac1  20028  pgpfac  20032  nrhmzr  20487  lidldvgen  21306  iunocv  21653  ismhp3  22102  istopg  22856  dfconn2  23380  1stccn  23424  iskgen3  23510  fbfinnfr  23802  iscmet3  25266  wilthlem3  27053  eqcuts2  27799  elons2  28271  onsfi  28369  isch3  31335  choc0  31420  pjnormssi  32262  reuxfrdf  32583  rabsspr  32594  rabsstp  32595  inpr0  32625  ssiun3  32651  ssdifidlprm  33557  fmcncfil  34115  bnj115  34908  bnj946  34957  bnj1211  34979  bnj1294  34999  bnj1385  35014  bnj110  35040  bnj611  35100  bnj864  35104  bnj865  35105  bnj1000  35123  bnj978  35131  bnj1049  35156  bnj1090  35161  bnj1133  35171  bnj1176  35187  bnj1186  35189  bnj1253  35199  bnj1388  35215  axprALT2  35293  axregs  35323  onvf1odlem4  35328  untuni  35931  dfon2lem8  36010  wzel  36044  dfrdg4  36173  ixpeq12dv  36438  cbvralvw2  36448  onsuct0  36663  regsfromregtr  36696  bj-ralvw  37154  bj-rcleqf  37300  bj-rep  37348  bj-axseprep  37349  bj-axreprepsep  37350  exrecfnlem  37661  fvineqsneq  37694  poimirlem25  37925  poimirlem30  37930  mptbi12f  38446  ralmo  38640  ralrmo3  38644  pmapglbx  40174  cdlemefrs29bpre0  40801  sn-axrep5v  42618  dford4  43415  unielss  43604  orddif0suc  43654  cllem0  43951  elmapintrab  43961  elintima  44038  ss2iundf  44044  ntrneiiso  44476  ntrneik2  44477  ntrneix2  44478  ntrneikb  44479  scottabf  44625  expandral  44675  ismnushort  44686  ralbidar  44829  rexbidar  44830  ssralv2  44916  en3lpVD  45229  ssralv2VD  45250  trintALTVD  45264  traxext  45362  dfac5prim  45375  permac8prim  45399  nregmodel  45402  ssrabf  45502  rabssf  45507  r19.3rzf  45546  rexrsb  47489  empty-surprise  50170  alsconv  50178