Definition df-ral 3047

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 47076 or ralndv2 47077, 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 3046	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1538	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 206	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  rgen  3048  raln  3054  alral  3060  ralimi2  3063  ral2imi  3070  ralbii2  3073  r19.26m  3092  r2allem  3123  hbralrimi  3125  ralimdv2  3144  ralbidv2  3154  r19.21vOLD  3161  r3al  3177  rspw  3216  cbvralvw  3217  rsp  3227  r19.21t  3233  r19.23t  3235  ralrimd  3244  nfra1  3263  ralcom4  3265  cbvralfw  3281  hbral  3285  nfraldw  3286  cbvralsvw  3293  raleqbidvvOLD  3311  cbvraldva2  3324  sbralie  3329  sbralieOLD  3331  raleqf  3332  cbvralf  3337  rgen2a  3348  nfrald  3349  ralcom2  3354  moelOLD  3382  rabbi  3442  rabid2f  3443  rabid2im  3444  rabid2OLD  3446  ralv  3483  ceqsralt  3491  rspct  3583  rspc  3585  rspcimdv  3587  rspc2gv  3607  ralxpxfr2d  3621  ralab  3672  ralab2  3676  ralrab2  3677  reu2  3704  reu6  3705  reu3  3706  rmo4  3709  reu8  3712  rmo3f  3713  rmoim  3719  2reuswap  3725  2reuswap2  3726  2reu5lem2  3735  2reu5lem3  3736  2rmoswap  3740  rmo2  3858  rmo3  3860  rmoanim  3865  cbvralcsf  3912  dfss3  3943  dfss3f  3946  ssralv  4023  ralss  4029  ssabral  4036  ss2rab  4042  rabss  4043  ssrab  4044  dfdif3OLD  4089  rexdifi  4121  ralunb  4168  reuss2  4297  rspn0  4327  n0el  4335  disj  4421  disj1  4423  r19.2z  4466  r19.3rz  4468  ralidmw  4479  rzal  4480  ralidm  4483  ralf0  4485  falseral0  4487  rabsssn  4640  ralsnsg  4642  ralsng  4647  unissb  4911  unissbOLD  4912  dfint2  4920  elint2  4925  elintrab  4932  ssintrab  4943  dfiin2g  5004  invdisj  5101  disjss3  5114  dftr5  5226  dftr5OLD  5227  reusv2lem4  5364  axprlem2  5387  axprlem4  5389  axprlem4OLD  5392  axprlem5OLD  5393  dffr6  5602  raliunxp  5811  dmopab3  5891  rnopab3  5928  asymref  6097  asymref2  6098  dfpo2  6277  dffun7  6551  funcnv  6593  fnres  6653  mptfnf  6661  fnopabg  6663  dff3  7079  dffo3  7081  dffo3f  7085  fnssintima  7344  imaeqalov  7635  find  7880  funcnvuni  7917  zfrep6  7942  ralxp3f  8125  frpoins3xpg  8128  frpoins3xp3g  8129  nfixpw  8893  nfixp  8894  marypha2lem3  9406  zfregcl  9565  zfinf2  9613  scottexs  9858  scott0s  9859  aceq1  10088  aceq2  10090  kmlem12  10133  kmlem14  10135  kmlem15  10136  zorn2lem4  10470  zorn2lem5  10471  ingru  10786  axgroth5  10795  grothprim  10805  sstskm  10813  supsrlem  11082  infm3  12158  nnunb  12454  nnwos  12888  fz1sbc  13574  cotr2g  14952  caubnd  15334  rpnnen2lem12  16200  isprm2  16658  pgpfac1  20018  pgpfac  20022  nrhmzr  20452  lidldvgen  21250  iunocv  21596  ismhp3  22035  istopg  22788  dfconn2  23312  1stccn  23356  iskgen3  23442  fbfinnfr  23734  iscmet3  25200  wilthlem3  26987  eqscut2  27725  elons2  28166  onsfi  28254  isch3  31177  choc0  31262  pjnormssi  32104  reuxfrdf  32427  rabsspr  32437  rabsstp  32438  inpr0  32468  ssiun3  32494  ssdifidlprm  33437  fmcncfil  33929  bnj115  34723  bnj946  34772  bnj1142  34787  bnj1211  34795  bnj1294  34815  bnj1385  34830  bnj110  34856  bnj611  34916  bnj864  34920  bnj865  34921  bnj1000  34939  bnj978  34947  bnj1049  34972  bnj1090  34977  bnj1133  34987  bnj1176  35003  bnj1186  35005  bnj1253  35015  bnj1388  35031  untuni  35693  dfon2lem8  35775  wzel  35809  dfrdg4  35936  ixpeq12dv  36201  cbvralvw2  36211  onsuct0  36426  bj-ralvw  36864  bj-rcleqf  37010  exrecfnlem  37364  fvineqsneq  37397  poimirlem25  37636  poimirlem30  37641  nninfnub  37742  mptbi12f  38157  pmapglbx  39755  cdlemefrs29bpre0  40382  sn-axrep5v  42196  dford4  42990  unielss  43179  orddif0suc  43229  cllem0  43527  elmapintrab  43537  elintima  43614  ss2iundf  43620  ntrneiiso  44052  ntrneik2  44053  ntrneix2  44054  ntrneikb  44055  scottabf  44201  expandral  44251  ismnushort  44262  ralbidar  44406  rexbidar  44407  ssralv2  44493  en3lpVD  44806  ssralv2VD  44827  trintALTVD  44841  traxext  44939  dfac5prim  44952  permac8prim  44976  nregmodel  44979  ssrabf  45080  rabssf  45085  r19.3rzf  45124  rexrsb  47071  empty-surprise  49648  alsconv  49656