Definition df-ral 3048

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 47135 or ralndv2 47136, 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 3047	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1539	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3049  raln  3055  alral  3061  ralimi2  3064  ral2imi  3071  ralbii2  3074  r19.26m  3091  r2allem  3120  hbralrimi  3122  ralimdv2  3141  ralbidv2  3151  r3al  3170  rspw  3209  cbvralvw  3210  rsp  3220  r19.21t  3226  r19.23t  3228  ralrimd  3237  nfra1  3256  ralcom4  3258  cbvralfw  3272  hbral  3276  nfraldw  3277  cbvralsvw  3283  raleqbidvvOLD  3301  cbvraldva2  3314  sbralie  3318  sbralieOLD  3320  raleqf  3321  cbvralf  3326  rgen2a  3337  nfrald  3338  ralcom2  3343  rabbi  3425  rabid2f  3426  rabid2im  3427  ralv  3463  ceqsralt  3471  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  4016  ss2rab  4021  rabss  4022  ssrab  4023  dfdif3OLD  4068  rexdifi  4100  ralunb  4147  reuss2  4276  rspn0  4306  n0el  4314  disj  4400  disj1  4402  r19.2z  4445  r19.3rz  4447  ralidmw  4458  rzal  4459  ralidm  4462  ralf0  4464  falseral0  4466  rabsssn  4621  ralsnsg  4623  ralsng  4628  unissb  4891  dfint2  4899  elint2  4904  elintrab  4910  ssintrab  4921  dfiin2g  4981  invdisj  5077  disjss3  5090  dftr5  5202  reusv2lem4  5339  axprlem2  5362  axprlem4  5364  axprlem4OLD  5367  axprlem5OLD  5368  dffr6  5572  raliunxp  5779  dmopab3  5859  rnopab3  5896  asymref  6063  asymref2  6064  dfpo2  6243  dffun7  6508  funcnv  6550  fnres  6608  mptfnf  6616  fnopabg  6618  dff3  7033  dffo3  7035  dffo3f  7039  fnssintima  7296  imaeqalov  7585  find  7825  funcnvuni  7862  zfrep6  7887  ralxp3f  8067  frpoins3xpg  8070  frpoins3xp3g  8071  nfixpw  8840  nfixp  8841  marypha2lem3  9321  zfregcl  9480  zfregclOLD  9481  zfinf2  9532  scottexs  9777  scott0s  9778  aceq1  10005  aceq2  10007  kmlem12  10050  kmlem14  10052  kmlem15  10053  zorn2lem4  10387  zorn2lem5  10388  ingru  10703  axgroth5  10712  grothprim  10722  sstskm  10730  supsrlem  10999  infm3  12078  nnunb  12374  nnwos  12810  fz1sbc  13497  cotr2g  14880  caubnd  15263  rpnnen2lem12  16131  isprm2  16590  pgpfac1  19992  pgpfac  19996  nrhmzr  20450  lidldvgen  21269  iunocv  21616  ismhp3  22055  istopg  22808  dfconn2  23332  1stccn  23376  iskgen3  23462  fbfinnfr  23754  iscmet3  25218  wilthlem3  27005  eqscut2  27745  elons2  28193  onsfi  28281  isch3  31216  choc0  31301  pjnormssi  32143  reuxfrdf  32465  rabsspr  32476  rabsstp  32477  inpr0  32507  ssiun3  32533  ssdifidlprm  33418  fmcncfil  33939  bnj115  34732  bnj946  34781  bnj1142  34796  bnj1211  34804  bnj1294  34824  bnj1385  34839  bnj110  34865  bnj611  34925  bnj864  34929  bnj865  34930  bnj1000  34948  bnj978  34956  bnj1049  34981  bnj1090  34986  bnj1133  34996  bnj1176  35012  bnj1186  35014  bnj1253  35024  bnj1388  35040  r1omhfbregs  35121  axregs  35133  onvf1odlem4  35138  untuni  35741  dfon2lem8  35823  wzel  35857  dfrdg4  35984  ixpeq12dv  36249  cbvralvw2  36259  onsuct0  36474  bj-ralvw  36912  bj-rcleqf  37058  exrecfnlem  37412  fvineqsneq  37445  poimirlem25  37684  poimirlem30  37689  nninfnub  37790  mptbi12f  38205  eqab2  38282  pmapglbx  39807  cdlemefrs29bpre0  40434  sn-axrep5v  42248  dford4  43061  unielss  43250  orddif0suc  43300  cllem0  43598  elmapintrab  43608  elintima  43685  ss2iundf  43691  ntrneiiso  44123  ntrneik2  44124  ntrneix2  44125  ntrneikb  44126  scottabf  44272  expandral  44322  ismnushort  44333  ralbidar  44476  rexbidar  44477  ssralv2  44563  en3lpVD  44876  ssralv2VD  44897  trintALTVD  44911  traxext  45009  dfac5prim  45022  permac8prim  45046  nregmodel  45049  ssrabf  45150  rabssf  45155  r19.3rzf  45194  rexrsb  47130  empty-surprise  49813  alsconv  49821