Definition df-ral 3078

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 47787 or ralndv2 47788, 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 3077	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1567	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1566	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 209	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3079  ralrid  3085  raln  3086  ralimi2  3095  ral2imi  3102  ralbii2  3105  r19.26m  3122  r2allem  3151  ralimdv2  3172  ralbidv2  3182  r3al  3201  rspw  3240  cbvralvw  3241  rsp  3251  r19.21t  3257  r19.23t  3259  ralrimd  3268  nfra1  3287  ralcom4  3289  cbvralfw  3303  hbral  3307  nfraldw  3308  cbvralsvw  3314  cbvraldva2  3338  sbralie  3340  sbralieOLD  3342  raleqf  3343  cbvralf  3347  rgen2a  3358  nfrald  3359  ralcom2  3364  rabbi  3444  rabid2f  3445  rabid2im  3446  ralv  3479  ceqsralt  3487  rspct  3566  rspc  3568  rspcimdv  3570  rspc2gv  3590  ralxpxfr2d  3604  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  3839  rmo3  3841  rmoanim  3847  cbvralcsf  3894  dfss3  3925  dfss3f  3928  ssralv  4005  ralss  4009  ssabral  4017  ss2rab  4022  rabss  4023  ssrab  4024  ss2rabd  4025  dfdif3OLD  4072  rexdifi  4103  ralunb  4149  reuss2  4278  rspn0  4310  n0el  4318  disj  4409  disj1  4411  rzal  4454  ralf0  4457  r19.2z  4459  r19.3rz  4461  falseral0OLD  4475  ralidmw  4476  ralidm  4477  rabsssn  4633  ralsnsg  4635  ralsng  4640  unissb  4905  dfint2  4913  elint2  4918  elintrab  4924  ssintrab  4935  dfiin2g  4994  invdisj  5094  disjss3  5107  dftr5  5221  zfrep6  5249  reusv2lem4  5372  axprlem2  5395  axprlem4OLD  5401  axprlem5OLD  5402  dffr6  5617  raliunxp  5825  dmopab3  5909  rnopab3  5946  asymref  6116  asymref2  6117  dfpo2  6297  dffun7  6563  funcnv  6605  fnres  6662  mptfnf  6670  fnopabg  6672  dff3  7095  dffo3  7097  dffo3f  7101  fnssintima  7360  imaeqalov  7649  find  7891  funcnvuni  7928  zfrep6OLD  7951  ralxp3f  8132  frpoins3xpg  8135  frpoins3xp3g  8136  nfixpw  8913  nfixp  8914  marypha2lem3  9396  zfregcl  9555  zfregclOLD  9556  zfinf2  9610  scottexs  9860  scott0s  9861  scottabf  9865  aceq1  10100  aceq2  10102  kmlem12  10144  kmlem14  10146  kmlem15  10147  zorn2lem4  10482  zorn2lem5  10483  axgroth5  10808  grothprim  10818  sstskm  10826  supsrlem  11095  infm3  12173  nnunb  12499  nnwos  12938  fz1sbc  13627  cotr2g  15012  caubnd  15409  rpnnen2lem12  16280  isprm2  16739  pgpfac1  20151  pgpfac  20155  nrhmzr  20621  ssdifidlprm  21465  lidldvgen  21481  iunocv  21810  ismhp3  22284  istopg  23031  dfconn2  23555  1stccn  23599  iskgen3  23685  fbfinnfr  23977  iscmet3  25431  wilthlem3  27210  eqcuts2  27955  elons2  28427  onsfi  28525  isch3  31559  choc0  31644  pjnormssi  32486  reuxfrdf  32803  rabsspr  32813  rabsstp  32814  inpr0  32844  ssiun3  32869  fmcncfil  34287  bnj115  35080  bnj946  35129  bnj1211  35151  bnj1294  35171  bnj1385  35186  bnj110  35212  bnj611  35272  bnj864  35276  bnj865  35277  bnj1000  35295  bnj978  35303  bnj1049  35328  bnj1090  35333  bnj1133  35343  bnj1176  35359  bnj1186  35361  bnj1253  35371  bnj1388  35387  axprALT2  35467  axregs  35506  onvf1odlem4  35544  untuni  36155  dfon2lem8  36234  wzel  36268  dfrdg4  36397  ixpeq12dv  36672  cbvralvw2  36682  onsuct0  36896  axtco  36926  axtco1g  36931  regsfromregtco  36993  mh-infprim2bi  37002  mh-infprim3bi  37003  bj-ralvw  37458  bj-rcleqf  37605  bj-rep  37654  bj-axseprep  37655  bj-axreprepsep  37656  exrecfnlem  37969  fvineqsneq  38002  poimirlem25  38240  poimirlem30  38245  mptbi12f  38761  ralmo  38955  ralrmo3  38959  pmapglbx  40489  cdlemefrs29bpre0  41116  sn-axrep5v  42934  dford4  43704  unielss  43893  orddif0suc  43943  cllem0  44240  elmapintrab  44250  elintima  44327  ss2iundf  44333  ntrneiiso  44765  ntrneik2  44766  ntrneix2  44767  ntrneikb  44768  expandral  44948  ismnushort  44959  ralbidar  45102  rexbidar  45103  ssralv2  45188  en3lpVD  45501  ssralv2VD  45522  trintALTVD  45536  traxext  45634  dfac5prim  45647  permac8prim  45671  nregmodel  45674  ssrabf  45780  rabssf  45785  r19.3rzf  45824  rexrsb  47782  empty-surprise  50505  dfrals2  50513  alsralrex  50535