Definition df-ral 3050

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 47541 or ralndv2 47542, 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 3049	. 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  3051  ralrid  3057  raln  3058  ralimi2  3067  ral2imi  3074  ralbii2  3077  r19.26m  3094  r2allem  3123  ralimdv2  3144  ralbidv2  3154  r3al  3173  rspw  3212  cbvralvw  3213  rsp  3223  r19.21t  3229  r19.23t  3231  ralrimd  3240  nfra1  3259  ralcom4  3261  cbvralfw  3275  hbral  3279  nfraldw  3280  cbvralsvw  3286  cbvraldva2  3311  sbralie  3313  sbralieOLD  3315  raleqf  3316  cbvralf  3320  rgen2a  3331  nfrald  3332  ralcom2  3337  rabbi  3417  rabid2f  3418  rabid2im  3419  ralv  3454  ceqsralt  3462  rspct  3548  rspc  3550  rspcimdv  3552  rspc2gv  3572  ralxpxfr2d  3586  ralab  3636  ralab2  3640  ralrab2  3641  reu2  3668  reu6  3669  reu3  3670  rmo4  3673  reu8  3676  rmo3f  3677  rmoim  3683  2reuswap  3689  2reuswap2  3690  2reu5lem2  3699  2reu5lem3  3700  2rmoswap  3704  rmo2  3821  rmo3  3823  rmoanim  3828  cbvralcsf  3875  dfss3  3906  dfss3f  3909  ssralv  3985  ralss  3989  ssabral  3997  ss2rab  4002  rabss  4003  ssrab  4004  ss2rabd  4005  dfdif3OLD  4051  rexdifi  4082  ralunb  4128  reuss2  4256  rspn0  4286  n0el  4294  disj  4380  disj1  4382  rzal  4424  ralf0  4427  r19.2z  4429  r19.3rz  4431  falseral0OLD  4445  ralidmw  4446  ralidm  4447  rabsssn  4602  ralsnsg  4604  ralsng  4609  unissb  4873  dfint2  4881  elint2  4886  elintrab  4892  ssintrab  4903  dfiin2g  4962  invdisj  5060  disjss3  5073  dftr5  5185  zfrep6  5213  reusv2lem4  5332  axprlem2  5355  axprlem4OLD  5361  axprlem5OLD  5362  dffr6  5576  raliunxp  5783  dmopab3  5863  rnopab3  5900  asymref  6068  asymref2  6069  dfpo2  6249  dffun7  6514  funcnv  6556  fnres  6614  mptfnf  6622  fnopabg  6624  dff3  7041  dffo3  7043  dffo3f  7047  fnssintima  7306  imaeqalov  7595  find  7835  funcnvuni  7872  zfrep6OLD  7897  ralxp3f  8076  frpoins3xpg  8079  frpoins3xp3g  8080  nfixpw  8853  nfixp  8854  marypha2lem3  9339  zfregcl  9498  zfregclOLD  9499  zfinf2  9552  scottexs  9800  scott0s  9801  aceq1  10028  aceq2  10030  kmlem12  10073  kmlem14  10075  kmlem15  10076  zorn2lem4  10410  zorn2lem5  10411  axgroth5  10736  grothprim  10746  sstskm  10754  supsrlem  11023  infm3  12104  nnunb  12422  nnwos  12854  fz1sbc  13543  cotr2g  14927  caubnd  15310  rpnnen2lem12  16181  isprm2  16640  pgpfac1  20046  pgpfac  20050  nrhmzr  20503  lidldvgen  21321  iunocv  21650  ismhp3  22097  istopg  22848  dfconn2  23372  1stccn  23416  iskgen3  23502  fbfinnfr  23794  iscmet3  25248  wilthlem3  27021  eqcuts2  27766  elons2  28238  onsfi  28336  isch3  31300  choc0  31385  pjnormssi  32227  reuxfrdf  32548  rabsspr  32559  rabsstp  32560  inpr0  32590  ssiun3  32616  ssdifidlprm  33506  fmcncfil  34063  bnj115  34856  bnj946  34905  bnj1211  34927  bnj1294  34947  bnj1385  34962  bnj110  34988  bnj611  35048  bnj864  35052  bnj865  35053  bnj1000  35071  bnj978  35079  bnj1049  35104  bnj1090  35109  bnj1133  35119  bnj1176  35135  bnj1186  35137  bnj1253  35147  bnj1388  35163  axprALT2  35241  axregs  35271  onvf1odlem4  35276  untuni  35879  dfon2lem8  35958  wzel  35992  dfrdg4  36121  ixpeq12dv  36386  cbvralvw2  36396  onsuct0  36611  axtco  36641  axtco1g  36646  regsfromregtco  36708  mh-infprim2bi  36717  mh-infprim3bi  36718  bj-ralvw  37174  bj-rcleqf  37320  bj-rep  37368  bj-axseprep  37369  bj-axreprepsep  37370  exrecfnlem  37683  fvineqsneq  37716  poimirlem25  37954  poimirlem30  37959  mptbi12f  38475  ralmo  38669  ralrmo3  38673  pmapglbx  40203  cdlemefrs29bpre0  40830  sn-axrep5v  42646  dford4  43445  unielss  43634  orddif0suc  43684  cllem0  43981  elmapintrab  43991  elintima  44068  ss2iundf  44074  ntrneiiso  44506  ntrneik2  44507  ntrneix2  44508  ntrneikb  44509  scottabf  44655  expandral  44705  ismnushort  44716  ralbidar  44859  rexbidar  44860  ssralv2  44946  en3lpVD  45259  ssralv2VD  45280  trintALTVD  45294  traxext  45392  dfac5prim  45405  permac8prim  45429  nregmodel  45432  ssrabf  45532  rabssf  45537  r19.3rzf  45576  rexrsb  47536  empty-surprise  50245  alsconv  50253