Definition df-ral 3077

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 48217 or ralndv2 48218, 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 3076	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1567	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 209	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is used by:  rgen  3078  ralrid  3084  raln  3085  ralimi2  3094  ral2imi  3101  ralbii2  3104  r19.26m  3121  r2allem  3150  ralimdv2  3171  ralbidv2  3181  r3al  3200  rspw  3239  cbvralvw  3240  rsp  3250  r19.21t  3256  r19.23t  3258  ralrimd  3267  nfra1  3286  ralcom4  3288  cbvralfw  3302  hbral  3306  nfraldw  3307  cbvralsvw  3313  cbvraldva2  3336  sbralie  3338  sbralieOLD  3340  raleqf  3341  cbvralf  3345  rgen2a  3356  nfrald  3357  ralcom2  3362  rabbi  3441  rabid2f  3442  rabid2im  3443  ralv  3476  ceqsralt  3484  rspct  3562  rspc  3564  rspcimdv  3566  rspc2gv  3585  ralxpxfr2d  3599  ralab  3650  ralab2  3654  ralrab2  3655  reu2  3682  reu6  3683  reu3  3684  rmo4  3687  reu8  3690  rmo3f  3691  rmoim  3697  2reuswap  3703  2reuswap2  3704  2reu5lem2  3713  2reu5lem3  3714  2rmoswap  3718  rmo2  3833  rmo3  3835  rmoanim  3841  cbvralcsf  3888  dfss3  3897  dfss3f  3900  ssralv  3977  ralss  3981  ssabral  3989  ss2rab  3994  rabss  3995  ssrab  3996  ss2rabd  3997  rexdifi  4086  ralunb  4195  reuss2  4271  rspn0  4303  n0el  4311  disj  4402  disj1  4404  rzal  4449  ralf0  4452  r19.2z  4454  r19.3rz  4456  falseral0OLD  4470  ralidmw  4471  ralidm  4472  rabsssn  4628  ralsnsg  4630  ralsng  4635  unissb  4900  dfint2  4908  elint2  4913  elintrab  4919  ssintrab  4930  dfiin2g  4988  invdisj  5088  disjss3  5101  dftr5  5215  zfrep6  5241  reusv2lem4  5362  axprlem2  5385  dffr6  5606  raliunxp  5815  dmopab3  5900  rnopab3  5937  asymref  6109  asymref2  6110  dfpo2  6299  dffun7  6567  funcnv  6609  fnres  6666  mptfnf  6674  fnopabg  6676  dff3  7100  dffo3  7102  dffo3f  7106  fnssintima  7372  imaeqalov  7660  find  7907  funcnvuni  7944  zfrep6OLD  7967  ralxp3f  8154  frpoins3xpg  8157  frpoins3xp3g  8158  nfixpw  8944  nfixp  8945  marypha2lem3  9429  zfregcl  9588  zfregclOLD  9589  zfinf2  9643  scottabf  9939  scottexsOLD  9943  scott0bsOLD  9945  aceq1  10196  aceq2  10198  kmlem12  10240  kmlem14  10242  kmlem15  10243  zorn2lem4  10577  zorn2lem5  10578  axgroth5  10909  grothprim  10919  sstskm  10927  supsrlem  11196  infm3  12276  nnunb  12602  nnwos  13042  fz1sbc  13734  cotr2g  15129  caubnd  15526  rpnnen2lem12  16393  isprm2  16857  pgpfac1  20296  pgpfac  20300  nrhmzr  20789  ssdifidlprm  21642  lidldvgen  21658  iunocv  21987  ismhp3  22463  istopg  23213  dfconn2  23737  1stccn  23782  iskgen3  23868  fbfinnfr  24160  iscmet3  25614  wilthlem3  27397  eqcuts2  28172  elons2  28644  onsfi  28742  isch3  31843  choc0  31928  pjnormssi  32770  reuxfrdf  33129  rabsspr  33139  rabsstp  33140  inpr0  33170  ssiun3  33195  fmcncfil  34605  bnj115  35398  bnj946  35447  bnj1211  35469  bnj1294  35489  bnj1385  35504  bnj110  35530  bnj611  35590  bnj864  35594  bnj865  35595  bnj1000  35613  bnj978  35621  bnj1049  35646  bnj1090  35651  bnj1133  35661  bnj1176  35677  bnj1186  35679  bnj1253  35689  bnj1388  35705  axprALT2  35776  axregs  35849  onvf1odlem4  35927  onprcf1acwevdlem1  35937  untuni  36516  dfon2lem8  36594  wzel  36628  dfrdg4  36757  ixpeq12dv  37047  cbvralvw2  37057  onsuct0  37271  axtco  37301  axtco1g  37306  regsfromregtco  37368  mh-infprim2bi  37377  mh-infprim3bi  37378  bj-ralvw  37833  bj-rcleqf  37980  bj-rep  38031  bj-axseprep  38032  bj-axreprepsep  38033  exrecfnlem  38345  fvineqsneq  38378  poimirlem25  38606  poimirlem30  38611  mptbi12f  39141  ralmo  39335  ralrmo3  39339  pmapglbx  40869  cdlemefrs29bpre0  41496  sn-axrep5v  43314  dford4  44078  unielss  44262  orddif0suc  44312  cllem0  44609  elmapintrab  44619  elintima  44695  ss2iundf  44701  ntrneiiso  45133  ntrneik2  45134  ntrneix2  45135  ntrneikb  45136  expandral  45316  ismnushort  45327  ralbidar  45470  rexbidar  45471  ssralv2  45556  en3lpVD  45869  ssralv2VD  45890  trintALTVD  45904  traxext  46009  dfac5prim  46022  permac8prim  46046  nregmodel  46049  ssrabf  46171  rabssf  46176  r19.3rzf  46215  rexrsb  48212  empty-surprise  50920  dfrals2  50928  alsralrex  50950  dfralseu2  50961