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 47544 or ralndv2 47545, 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  cbvraldva2  3314  sbralie  3316  sbralieOLD  3318  raleqf  3319  cbvralf  3323  rgen2a  3334  nfrald  3335  ralcom2  3340  rabbi  3420  rabid2f  3421  rabid2im  3422  ralv  3457  ceqsralt  3465  rspct  3551  rspc  3553  rspcimdv  3555  rspc2gv  3575  ralxpxfr2d  3589  ralab  3640  ralab2  3644  ralrab2  3645  reu2  3672  reu6  3673  reu3  3674  rmo4  3677  reu8  3680  rmo3f  3681  rmoim  3687  2reuswap  3693  2reuswap2  3694  2reu5lem2  3703  2reu5lem3  3704  2rmoswap  3708  rmo2  3826  rmo3  3828  rmoanim  3833  cbvralcsf  3880  dfss3  3911  dfss3f  3914  ssralv  3991  ralss  3997  ssabral  4005  ss2rab  4010  rabss  4011  ssrab  4012  ss2rabd  4013  dfdif3OLD  4059  rexdifi  4091  ralunb  4138  reuss2  4267  rspn0  4297  n0el  4305  disj  4391  disj1  4393  rzal  4435  ralf0  4438  r19.2z  4440  r19.3rz  4442  falseral0OLD  4456  ralidmw  4457  ralidm  4458  rabsssn  4613  ralsnsg  4615  ralsng  4620  unissb  4884  dfint2  4892  elint2  4897  elintrab  4903  ssintrab  4914  dfiin2g  4974  invdisj  5072  disjss3  5085  dftr5  5197  zfrep6  5225  reusv2lem4  5342  axprlem2  5365  axprlem4OLD  5371  axprlem5OLD  5372  dffr6  5584  raliunxp  5792  dmopab3  5872  rnopab3  5909  asymref  6077  asymref2  6078  dfpo2  6258  dffun7  6523  funcnv  6565  fnres  6623  mptfnf  6631  fnopabg  6633  dff3  7050  dffo3  7052  dffo3f  7056  fnssintima  7314  imaeqalov  7603  find  7843  funcnvuni  7880  zfrep6OLD  7905  ralxp3f  8084  frpoins3xpg  8087  frpoins3xp3g  8088  nfixpw  8861  nfixp  8862  marypha2lem3  9347  zfregcl  9506  zfregclOLD  9507  zfinf2  9560  scottexs  9808  scott0s  9809  aceq1  10036  aceq2  10038  kmlem12  10081  kmlem14  10083  kmlem15  10084  zorn2lem4  10418  zorn2lem5  10419  axgroth5  10744  grothprim  10754  sstskm  10762  supsrlem  11031  infm3  12112  nnunb  12430  nnwos  12862  fz1sbc  13551  cotr2g  14935  caubnd  15318  rpnnen2lem12  16189  isprm2  16648  pgpfac1  20054  pgpfac  20058  nrhmzr  20511  lidldvgen  21329  iunocv  21658  ismhp3  22105  istopg  22857  dfconn2  23381  1stccn  23425  iskgen3  23511  fbfinnfr  23803  iscmet3  25257  wilthlem3  27030  eqcuts2  27775  elons2  28247  onsfi  28345  isch3  31309  choc0  31394  pjnormssi  32236  reuxfrdf  32557  rabsspr  32568  rabsstp  32569  inpr0  32599  ssiun3  32625  ssdifidlprm  33515  fmcncfil  34072  bnj115  34865  bnj946  34914  bnj1211  34936  bnj1294  34956  bnj1385  34971  bnj110  34997  bnj611  35057  bnj864  35061  bnj865  35062  bnj1000  35080  bnj978  35088  bnj1049  35113  bnj1090  35118  bnj1133  35128  bnj1176  35144  bnj1186  35146  bnj1253  35156  bnj1388  35172  axprALT2  35250  axregs  35280  onvf1odlem4  35285  untuni  35888  dfon2lem8  35967  wzel  36001  dfrdg4  36130  ixpeq12dv  36395  cbvralvw2  36405  onsuct0  36620  axtco  36650  axtco1g  36655  regsfromregtco  36717  mh-infprim2bi  36726  mh-infprim3bi  36727  bj-ralvw  37183  bj-rcleqf  37329  bj-rep  37377  bj-axseprep  37378  bj-axreprepsep  37379  exrecfnlem  37692  fvineqsneq  37725  poimirlem25  37963  poimirlem30  37968  mptbi12f  38484  ralmo  38678  ralrmo3  38682  pmapglbx  40212  cdlemefrs29bpre0  40839  sn-axrep5v  42655  dford4  43454  unielss  43643  orddif0suc  43693  cllem0  43990  elmapintrab  44000  elintima  44077  ss2iundf  44083  ntrneiiso  44515  ntrneik2  44516  ntrneix2  44517  ntrneikb  44518  scottabf  44664  expandral  44714  ismnushort  44725  ralbidar  44868  rexbidar  44869  ssralv2  44955  en3lpVD  45268  ssralv2VD  45289  trintALTVD  45303  traxext  45401  dfac5prim  45414  permac8prim  45438  nregmodel  45441  ssrabf  45541  rabssf  45546  r19.3rzf  45585  rexrsb  47539  empty-surprise  50248  alsconv  50256