Definition df-ral 3053

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 47418 or ralndv2 47419, 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 3052	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1540	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3054  raln  3060  alral  3066  ralimi2  3069  ral2imi  3076  ralbii2  3079  r19.26m  3096  r2allem  3125  hbralrimi  3127  ralimdv2  3146  ralbidv2  3156  r3al  3175  rspw  3214  cbvralvw  3215  rsp  3225  r19.21t  3231  r19.23t  3233  ralrimd  3242  nfra1  3261  ralcom4  3263  cbvralfw  3277  hbral  3281  nfraldw  3282  cbvralsvw  3288  raleqbidvvOLD  3306  cbvraldva2  3319  sbralie  3323  sbralieOLD  3325  raleqf  3326  cbvralf  3331  rgen2a  3342  nfrald  3343  ralcom2  3348  rabbi  3430  rabid2f  3431  rabid2im  3432  ralv  3468  ceqsralt  3476  rspct  3563  rspc  3565  rspcimdv  3567  rspc2gv  3587  ralxpxfr2d  3601  ralab  3652  ralab2  3656  ralrab2  3657  reu2  3684  reu6  3685  reu3  3686  rmo4  3689  reu8  3692  rmo3f  3693  rmoim  3699  2reuswap  3705  2reuswap2  3706  2reu5lem2  3715  2reu5lem3  3716  2rmoswap  3720  rmo2  3838  rmo3  3840  rmoanim  3845  cbvralcsf  3892  dfss3  3923  dfss3f  3926  ssralv  4003  ralss  4009  ssabral  4017  ss2rab  4022  rabss  4023  ssrab  4024  ss2rabd  4025  dfdif3OLD  4071  rexdifi  4103  ralunb  4150  reuss2  4279  rspn0  4309  n0el  4317  disj  4403  disj1  4405  rzal  4448  ralf0  4451  r19.2z  4453  r19.3rz  4455  falseral0OLD  4469  ralidmw  4470  ralidm  4471  rabsssn  4626  ralsnsg  4628  ralsng  4633  unissb  4897  dfint2  4905  elint2  4910  elintrab  4916  ssintrab  4927  dfiin2g  4987  invdisj  5085  disjss3  5098  dftr5  5210  reusv2lem4  5347  axprlem2  5370  axprlem4  5372  axprlem4OLD  5375  axprlem5OLD  5376  dffr6  5581  raliunxp  5789  dmopab3  5869  rnopab3  5906  asymref  6074  asymref2  6075  dfpo2  6255  dffun7  6520  funcnv  6562  fnres  6620  mptfnf  6628  fnopabg  6630  dff3  7047  dffo3  7049  dffo3f  7053  fnssintima  7310  imaeqalov  7599  find  7839  funcnvuni  7876  zfrep6  7901  ralxp3f  8081  frpoins3xpg  8084  frpoins3xp3g  8085  nfixpw  8858  nfixp  8859  marypha2lem3  9344  zfregcl  9503  zfregclOLD  9504  zfinf2  9555  scottexs  9803  scott0s  9804  aceq1  10031  aceq2  10033  kmlem12  10076  kmlem14  10078  kmlem15  10079  zorn2lem4  10413  zorn2lem5  10414  ingru  10730  axgroth5  10739  grothprim  10749  sstskm  10757  supsrlem  11026  infm3  12105  nnunb  12401  nnwos  12832  fz1sbc  13520  cotr2g  14903  caubnd  15286  rpnnen2lem12  16154  isprm2  16613  pgpfac1  20015  pgpfac  20019  nrhmzr  20474  lidldvgen  21293  iunocv  21640  ismhp3  22089  istopg  22843  dfconn2  23367  1stccn  23411  iskgen3  23497  fbfinnfr  23789  iscmet3  25253  wilthlem3  27040  eqcuts2  27786  elons2  28258  onsfi  28356  isch3  31320  choc0  31405  pjnormssi  32247  reuxfrdf  32568  rabsspr  32579  rabsstp  32580  inpr0  32610  ssiun3  32636  ssdifidlprm  33541  fmcncfil  34090  bnj115  34883  bnj946  34932  bnj1142  34947  bnj1211  34955  bnj1294  34975  bnj1385  34990  bnj110  35016  bnj611  35076  bnj864  35080  bnj865  35081  bnj1000  35099  bnj978  35107  bnj1049  35132  bnj1090  35137  bnj1133  35147  bnj1176  35163  bnj1186  35165  bnj1253  35175  bnj1388  35191  r1omhfb  35270  r1omhfbregs  35295  axregs  35297  onvf1odlem4  35302  untuni  35905  dfon2lem8  35984  wzel  36018  dfrdg4  36147  ixpeq12dv  36412  cbvralvw2  36422  onsuct0  36637  regsfromregtr  36670  bj-ralvw  37082  bj-rcleqf  37228  exrecfnlem  37586  fvineqsneq  37619  poimirlem25  37848  poimirlem30  37853  nninfnub  37954  mptbi12f  38369  eqab2  38453  ralmo  38563  ralrmo3  38567  pmapglbx  40097  cdlemefrs29bpre0  40724  sn-axrep5v  42541  dford4  43338  unielss  43527  orddif0suc  43577  cllem0  43874  elmapintrab  43884  elintima  43961  ss2iundf  43967  ntrneiiso  44399  ntrneik2  44400  ntrneix2  44401  ntrneikb  44402  scottabf  44548  expandral  44598  ismnushort  44609  ralbidar  44752  rexbidar  44753  ssralv2  44839  en3lpVD  45152  ssralv2VD  45173  trintALTVD  45187  traxext  45285  dfac5prim  45298  permac8prim  45322  nregmodel  45325  ssrabf  45425  rabssf  45430  r19.3rzf  45469  rexrsb  47413  empty-surprise  50094  alsconv  50102