Definition df-ral 3079

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 47980 or ralndv2 47981, 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 3078	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1568	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 209	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is used by:  rgen  3080  ralrid  3086  raln  3087  ralimi2  3096  ral2imi  3103  ralbii2  3106  r19.26m  3123  r2allem  3152  ralimdv2  3173  ralbidv2  3183  r3al  3202  rspw  3241  cbvralvw  3242  rsp  3252  r19.21t  3258  r19.23t  3260  ralrimd  3269  nfra1  3288  ralcom4  3290  cbvralfw  3304  hbral  3308  nfraldw  3309  cbvralsvw  3315  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  3565  rspc  3567  rspcimdv  3569  rspc2gv  3589  ralxpxfr2d  3603  ralab  3654  ralab2  3658  ralrab2  3659  reu2  3686  reu6  3687  reu3  3688  rmo4  3691  reu8  3694  rmo3f  3695  rmoim  3701  2reuswap  3707  2reuswap2  3708  2reu5lem2  3717  2reu5lem3  3718  2rmoswap  3722  rmo2  3837  rmo3  3839  rmoanim  3845  cbvralcsf  3892  dfss3  3923  dfss3f  3926  ssralv  4003  ralss  4007  ssabral  4015  ss2rab  4020  rabss  4021  ssrab  4022  ss2rabd  4023  rexdifi  4100  ralunb  4146  reuss2  4275  rspn0  4307  n0el  4315  disj  4406  disj1  4408  rzal  4453  ralf0  4456  r19.2z  4458  r19.3rz  4460  falseral0OLD  4474  ralidmw  4475  ralidm  4476  rabsssn  4632  ralsnsg  4634  ralsng  4639  unissb  4904  dfint2  4912  elint2  4917  elintrab  4923  ssintrab  4934  dfiin2g  4993  invdisj  5093  disjss3  5106  dftr5  5220  zfrep6  5248  reusv2lem4  5370  axprlem2  5393  axprlem4OLD  5399  axprlem5OLD  5400  dffr6  5615  raliunxp  5823  dmopab3  5907  rnopab3  5944  asymref  6114  asymref2  6115  dfpo2  6298  dffun7  6564  funcnv  6606  fnres  6663  mptfnf  6671  fnopabg  6673  dff3  7096  dffo3  7098  dffo3f  7102  fnssintima  7368  imaeqalov  7656  find  7895  funcnvuni  7932  zfrep6OLD  7955  ralxp3f  8138  frpoins3xpg  8141  frpoins3xp3g  8142  nfixpw  8926  nfixp  8927  marypha2lem3  9410  zfregcl  9569  zfregclOLD  9570  zfinf2  9624  scottabf  9881  scottexsOLD  9885  scott0bsOLD  9887  aceq1  10123  aceq2  10125  kmlem12  10167  kmlem14  10169  kmlem15  10170  zorn2lem4  10504  zorn2lem5  10505  axgroth5  10836  grothprim  10846  sstskm  10854  supsrlem  11123  infm3  12201  nnunb  12527  nnwos  12967  fz1sbc  13657  cotr2g  15051  caubnd  15448  rpnnen2lem12  16317  isprm2  16776  pgpfac1  20210  pgpfac  20214  nrhmzr  20700  ssdifidlprm  21550  lidldvgen  21566  iunocv  21895  ismhp3  22371  istopg  23121  dfconn2  23645  1stccn  23690  iskgen3  23776  fbfinnfr  24068  iscmet3  25522  wilthlem3  27304  eqcuts2  28049  elons2  28521  onsfi  28619  isch3  31708  choc0  31793  pjnormssi  32635  reuxfrdf  32952  rabsspr  32962  rabsstp  32963  inpr0  32993  ssiun3  33018  fmcncfil  34428  bnj115  35222  bnj946  35271  bnj1211  35293  bnj1294  35313  bnj1385  35328  bnj110  35354  bnj611  35414  bnj864  35418  bnj865  35419  bnj1000  35437  bnj978  35445  bnj1049  35470  bnj1090  35475  bnj1133  35485  bnj1176  35501  bnj1186  35503  bnj1253  35513  bnj1388  35529  axprALT2  35604  axregs  35652  onvf1odlem4  35690  untuni  36275  dfon2lem8  36354  wzel  36388  dfrdg4  36517  ixpeq12dv  36823  cbvralvw2  36833  onsuct0  37047  axtco  37077  axtco1g  37082  regsfromregtco  37144  mh-infprim2bi  37153  mh-infprim3bi  37154  bj-ralvw  37609  bj-rcleqf  37756  bj-rep  37805  bj-axseprep  37806  bj-axreprepsep  37807  exrecfnlem  38120  fvineqsneq  38153  poimirlem25  38381  poimirlem30  38386  mptbi12f  38901  ralmo  39095  ralrmo3  39099  pmapglbx  40629  cdlemefrs29bpre0  41256  sn-axrep5v  43074  dford4  43857  unielss  44046  orddif0suc  44096  cllem0  44393  elmapintrab  44403  elintima  44480  ss2iundf  44486  ntrneiiso  44918  ntrneik2  44919  ntrneix2  44920  ntrneikb  44921  expandral  45101  ismnushort  45112  ralbidar  45255  rexbidar  45256  ssralv2  45341  en3lpVD  45654  ssralv2VD  45675  trintALTVD  45689  traxext  45787  dfac5prim  45800  permac8prim  45824  nregmodel  45827  ssrabf  45933  rabssf  45938  r19.3rzf  45977  rexrsb  47975  empty-surprise  50698  dfrals2  50706  alsralrex  50728  dfralseu2  50739