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 48097 or ralndv2 48098, 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 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  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  3919  dfss3f  3922  ssralv  3999  ralss  4003  ssabral  4011  ss2rab  4016  rabss  4017  ssrab  4018  ss2rabd  4019  rexdifi  4096  ralunb  4142  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  5603  raliunxp  5812  dmopab3  5897  rnopab3  5934  asymref  6104  asymref2  6105  dfpo2  6288  dffun7  6555  funcnv  6597  fnres  6654  mptfnf  6662  fnopabg  6664  dff3  7088  dffo3  7090  dffo3f  7094  fnssintima  7360  imaeqalov  7648  find  7890  funcnvuni  7927  zfrep6OLD  7950  ralxp3f  8132  frpoins3xpg  8135  frpoins3xp3g  8136  nfixpw  8922  nfixp  8923  marypha2lem3  9407  zfregcl  9566  zfregclOLD  9567  zfinf2  9621  scottabf  9910  scottexsOLD  9914  scott0bsOLD  9916  aceq1  10167  aceq2  10169  kmlem12  10211  kmlem14  10213  kmlem15  10214  zorn2lem4  10548  zorn2lem5  10549  axgroth5  10880  grothprim  10890  sstskm  10898  supsrlem  11167  infm3  12245  nnunb  12571  nnwos  13011  fz1sbc  13702  cotr2g  15096  caubnd  15493  rpnnen2lem12  16360  isprm2  16819  pgpfac1  20257  pgpfac  20261  nrhmzr  20750  ssdifidlprm  21603  lidldvgen  21619  iunocv  21948  ismhp3  22424  istopg  23174  dfconn2  23698  1stccn  23743  iskgen3  23829  fbfinnfr  24121  iscmet3  25575  wilthlem3  27360  eqcuts2  28105  elons2  28577  onsfi  28675  isch3  31776  choc0  31861  pjnormssi  32703  reuxfrdf  33020  rabsspr  33030  rabsstp  33031  inpr0  33061  ssiun3  33086  fmcncfil  34496  bnj115  35290  bnj946  35339  bnj1211  35361  bnj1294  35381  bnj1385  35396  bnj110  35422  bnj611  35482  bnj864  35486  bnj865  35487  bnj1000  35505  bnj978  35513  bnj1049  35538  bnj1090  35543  bnj1133  35553  bnj1176  35569  bnj1186  35571  bnj1253  35581  bnj1388  35597  axprALT2  35664  axregs  35732  onvf1odlem4  35810  untuni  36395  dfon2lem8  36474  wzel  36508  dfrdg4  36637  ixpeq12dv  36927  cbvralvw2  36937  onsuct0  37151  axtco  37181  axtco1g  37186  regsfromregtco  37248  mh-infprim2bi  37257  mh-infprim3bi  37258  bj-ralvw  37713  bj-rcleqf  37860  bj-rep  37909  bj-axseprep  37910  bj-axreprepsep  37911  exrecfnlem  38222  fvineqsneq  38255  poimirlem25  38483  poimirlem30  38488  mptbi12f  39018  ralmo  39212  ralrmo3  39216  pmapglbx  40746  cdlemefrs29bpre0  41373  sn-axrep5v  43191  dford4  43974  unielss  44163  orddif0suc  44213  cllem0  44510  elmapintrab  44520  elintima  44597  ss2iundf  44603  ntrneiiso  45035  ntrneik2  45036  ntrneix2  45037  ntrneikb  45038  expandral  45218  ismnushort  45229  ralbidar  45372  rexbidar  45373  ssralv2  45458  en3lpVD  45771  ssralv2VD  45792  trintALTVD  45806  traxext  45904  dfac5prim  45917  permac8prim  45941  nregmodel  45944  ssrabf  46050  rabssf  46055  r19.3rzf  46094  rexrsb  48092  empty-surprise  50800  dfrals2  50808  alsralrex  50830  dfralseu2  50841