Definition df-ral 3056

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 47580 or ralndv2 47581, 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 3055	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1547	. . . . 5 class 𝑥
6	5, 3	wcel 2121	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1546	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 208	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3057  ralrid  3063  raln  3064  ralimi2  3073  ral2imi  3080  ralbii2  3083  r19.26m  3100  r2allem  3129  ralimdv2  3150  ralbidv2  3160  r3al  3179  rspw  3218  cbvralvw  3219  rsp  3229  r19.21t  3235  r19.23t  3237  ralrimd  3246  nfra1  3265  ralcom4  3267  cbvralfw  3281  hbral  3285  nfraldw  3286  cbvralsvw  3292  cbvraldva2  3317  sbralie  3319  sbralieOLD  3321  raleqf  3322  cbvralf  3326  rgen2a  3337  nfrald  3338  ralcom2  3343  rabbi  3423  rabid2f  3424  rabid2im  3425  ralv  3459  ceqsralt  3467  rspct  3547  rspc  3549  rspcimdv  3551  rspc2gv  3571  ralxpxfr2d  3585  ralab  3635  ralab2  3639  ralrab2  3640  reu2  3667  reu6  3668  reu3  3669  rmo4  3672  reu8  3675  rmo3f  3676  rmoim  3682  2reuswap  3688  2reuswap2  3689  2reu5lem2  3698  2reu5lem3  3699  2rmoswap  3703  rmo2  3820  rmo3  3822  rmoanim  3827  cbvralcsf  3874  dfss3  3905  dfss3f  3908  ssralv  3985  ralss  3989  ssabral  3997  ss2rab  4002  rabss  4003  ssrab  4004  ss2rabd  4005  dfdif3OLD  4051  rexdifi  4082  ralunb  4128  reuss2  4256  rspn0  4286  n0el  4294  disj  4380  disj1  4382  rzal  4424  ralf0  4427  r19.2z  4429  r19.3rz  4431  falseral0OLD  4445  ralidmw  4446  ralidm  4447  rabsssn  4602  ralsnsg  4604  ralsng  4609  unissb  4873  dfint2  4881  elint2  4886  elintrab  4892  ssintrab  4903  dfiin2g  4962  invdisj  5060  disjss3  5073  dftr5  5185  zfrep6  5213  reusv2lem4  5332  axprlem2  5355  axprlem4OLD  5361  axprlem5OLD  5362  dffr6  5576  raliunxp  5783  dmopab3  5867  rnopab3  5904  asymref  6072  asymref2  6073  dfpo2  6250  dffun7  6515  funcnv  6557  fnres  6615  mptfnf  6623  fnopabg  6625  dff3  7044  dffo3  7046  dffo3f  7050  fnssintima  7309  imaeqalov  7598  find  7839  funcnvuni  7876  zfrep6OLD  7899  ralxp3f  8079  frpoins3xpg  8082  frpoins3xp3g  8083  nfixpw  8858  nfixp  8859  marypha2lem3  9344  zfregcl  9503  zfregclOLD  9504  zfinf2  9558  scottexs  9806  scott0s  9807  aceq1  10034  aceq2  10036  kmlem12  10079  kmlem14  10081  kmlem15  10082  zorn2lem4  10417  zorn2lem5  10418  axgroth5  10743  grothprim  10753  sstskm  10761  supsrlem  11030  infm3  12110  nnunb  12428  nnwos  12860  fz1sbc  13549  cotr2g  14933  caubnd  15316  rpnnen2lem12  16187  isprm2  16646  pgpfac1  20051  pgpfac  20055  nrhmzr  20512  lidldvgen  21330  iunocv  21659  ismhp3  22133  istopg  22881  dfconn2  23405  1stccn  23449  iskgen3  23535  fbfinnfr  23827  iscmet3  25281  wilthlem3  27054  eqcuts2  27798  elons2  28270  onsfi  28368  isch3  31332  choc0  31417  pjnormssi  32259  reuxfrdf  32580  rabsspr  32591  rabsstp  32592  inpr0  32622  ssiun3  32649  ssdifidlprm  33543  fmcncfil  34125  bnj115  34921  bnj946  34970  bnj1211  34992  bnj1294  35012  bnj1385  35027  bnj110  35053  bnj611  35113  bnj864  35117  bnj865  35118  bnj1000  35136  bnj978  35144  bnj1049  35169  bnj1090  35174  bnj1133  35184  bnj1176  35200  bnj1186  35202  bnj1253  35212  bnj1388  35228  axprALT2  35303  axregs  35333  onvf1odlem4  35347  untuni  35950  dfon2lem8  36029  wzel  36063  dfrdg4  36192  ixpeq12dv  36457  cbvralvw2  36467  onsuct0  36682  axtco  36712  axtco1g  36717  regsfromregtco  36779  mh-infprim2bi  36788  mh-infprim3bi  36789  bj-ralvw  37245  bj-rcleqf  37391  bj-rep  37439  bj-axseprep  37440  bj-axreprepsep  37441  exrecfnlem  37754  fvineqsneq  37787  poimirlem25  38025  poimirlem30  38030  mptbi12f  38546  ralmo  38740  ralrmo3  38744  pmapglbx  40274  cdlemefrs29bpre0  40901  sn-axrep5v  42717  dford4  43487  unielss  43676  orddif0suc  43726  cllem0  44023  elmapintrab  44033  elintima  44110  ss2iundf  44116  ntrneiiso  44548  ntrneik2  44549  ntrneix2  44550  ntrneikb  44551  scottabf  44697  expandral  44747  ismnushort  44758  ralbidar  44901  rexbidar  44902  ssralv2  44988  en3lpVD  45301  ssralv2VD  45322  trintALTVD  45336  traxext  45434  dfac5prim  45447  permac8prim  45471  nregmodel  45474  ssrabf  45573  rabssf  45578  r19.3rzf  45617  rexrsb  47575  empty-surprise  50284  alsconv  50292