Definition df-ral 3068

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 47020 or ralndv2 47021, 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 3067	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1535	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3069  raln  3075  alral  3081  ralimi2  3084  ral2imi  3091  ralbii2  3095  ralrexbidOLD  3113  r19.26m  3116  r2allem  3148  hbralrimi  3150  ralimdv2  3169  ralbidv2  3180  r19.21vOLD  3187  r3al  3203  rspw  3242  cbvralvw  3243  rsp  3253  r19.21t  3259  r19.23t  3261  ralrimd  3270  ralbidaOLD  3277  nfra1  3290  ralcom4  3292  ralcom4OLD  3293  nfra2wOLD  3306  cbvralfw  3310  hbral  3314  nfraldw  3315  cbvralsvw  3323  nfraldwOLD  3328  raleqbidvvOLD  3343  cbvraldva2  3356  raleqf  3361  sbralie  3366  cbvralf  3368  rgen2a  3379  nfrald  3380  ralcom2  3385  moelOLD  3413  rabbi  3475  rabid2f  3476  rabid2im  3477  rabid2OLD  3479  ralv  3516  ceqsralt  3524  rspct  3621  rspc  3623  rspcimdv  3625  rspc2gv  3645  ralxpxfr2d  3659  ralab  3713  ralabOLD  3714  ralab2  3719  ralrab2  3720  reu2  3747  reu6  3748  reu3  3749  rmo4  3752  reu8  3755  rmo3f  3756  rmoim  3762  2reuswap  3768  2reuswap2  3769  2reu5lem2  3778  2reu5lem3  3779  2rmoswap  3783  rmo2  3909  rmo3  3911  rmoanim  3916  cbvralcsf  3966  dfss3  3997  dfss3f  4000  ssralv  4077  ssabral  4088  ss2rab  4094  rabss  4095  ssrab  4096  dfdif3OLD  4141  rexdifi  4173  ralunb  4220  reuss2  4345  rspn0  4379  n0el  4387  disj  4473  disj1  4475  r19.2z  4518  r19.3rz  4520  ralidmw  4531  rzal  4532  ralidm  4535  ralf0  4537  falseral0  4539  rabsssn  4690  ralsnsg  4692  ralsng  4697  unissb  4963  unissbOLD  4964  dfint2  4972  elint2  4977  elintrab  4984  ssintrab  4995  dfiin2g  5055  invdisj  5152  disjss3  5165  dftr5  5287  dftr5OLD  5288  reusv2lem4  5419  axprlem2  5442  axprlem4  5444  axprlem5  5445  dffr6  5655  raliunxp  5864  dmopab3  5944  asymref  6148  asymref2  6149  dfpo2  6327  dffun7  6605  funcnv  6647  fnres  6707  mptfnf  6715  fnopabg  6717  dff3  7134  dffo3  7136  dffo3f  7140  fnssintima  7398  imaeqalov  7689  find  7935  funcnvuni  7972  zfrep6  7995  ralxp3f  8178  frpoins3xpg  8181  frpoins3xp3g  8182  nfixpw  8974  nfixp  8975  marypha2lem3  9506  zfregcl  9663  zfinf2  9711  scottexs  9956  scott0s  9957  aceq1  10186  aceq2  10188  kmlem12  10231  kmlem14  10233  kmlem15  10234  zorn2lem4  10568  zorn2lem5  10569  ingru  10884  axgroth5  10893  grothprim  10903  sstskm  10911  supsrlem  11180  infm3  12254  nnunb  12549  nnwos  12980  fz1sbc  13660  cotr2g  15025  caubnd  15407  rpnnen2lem12  16273  isprm2  16729  pgpfac1  20124  pgpfac  20128  nrhmzr  20563  lidldvgen  21367  iunocv  21722  ismhp3  22169  istopg  22922  dfconn2  23448  1stccn  23492  iskgen3  23578  fbfinnfr  23870  iscmet3  25346  wilthlem3  27131  eqscut2  27869  elons2  28299  isch3  31273  choc0  31358  pjnormssi  32200  reuxfrdf  32519  rabsspr  32529  rabsstp  32530  inpr0  32560  ssiun3  32581  ssdifidlprm  33451  fmcncfil  33877  bnj115  34701  bnj946  34750  bnj1142  34765  bnj1211  34773  bnj1294  34793  bnj1385  34808  bnj110  34834  bnj611  34894  bnj864  34898  bnj865  34899  bnj1000  34917  bnj978  34925  bnj1049  34950  bnj1090  34955  bnj1133  34965  bnj1176  34981  bnj1186  34983  bnj1253  34993  bnj1388  35009  untuni  35671  dfon2lem8  35754  wzel  35788  dfrdg4  35915  ixpeq12dv  36182  cbvralvw2  36192  onsuct0  36407  bj-ralvw  36845  bj-rcleqf  36991  exrecfnlem  37345  fvineqsneq  37378  poimirlem25  37605  poimirlem30  37610  nninfnub  37711  mptbi12f  38126  pmapglbx  39726  cdlemefrs29bpre0  40353  sn-axrep5v  42209  dford4  42986  unielss  43179  orddif0suc  43230  cllem0  43528  elmapintrab  43538  elintima  43615  ss2iundf  43621  ntrneiiso  44053  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  scottabf  44209  expandral  44259  ismnushort  44270  ralbidar  44414  rexbidar  44415  ssralv2  44502  en3lpVD  44816  ssralv2VD  44837  trintALTVD  44851  traxext  44910  ssrabf  45016  rabssf  45021  r19.3rzf  45063  rexrsb  47015  empty-surprise  48876  alsconv  48884