Definition df-ral 2305

Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)

Assertion

Ref	Expression
df-ral	⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))

Detailed syntax breakdown of Definition df-ral

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wral 2300	. 2 wff ∀x ∈ A φ
5	2	cv 1241	. . . . 5 class x
6	5, 3	wcel 1390	. . . 4 wff x ∈ A
7	6, 1	wi 4	. . 3 wff (x ∈ A → φ)
8	7, 2	wal 1240	. 2 wff ∀x(x ∈ A → φ)
9	4, 8	wb 98	1 wff (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))

This definition is referenced by:  ralnex  2310  rexnalim  2311  ralbida  2314  ralbidv2  2322  ralbii2  2328  r2alf  2335  hbral  2347  hbra1  2348  nfra1  2349  nfraldxy  2350  nfraldya  2352  r3al  2360  alral  2361  rsp  2363  rgen  2368  rgen2a  2369  ralim  2374  ralimi2  2375  ralimdaa  2380  ralimdv2  2383  ralrimi  2384  r19.21t  2388  ralrimd  2391  r19.21bi  2401  rexim  2407  r19.23t  2417  r19.26m  2438  r19.32r  2451  rabid2  2480  rabbi  2481  raleqf  2495  cbvralf  2521  cbvraldva2  2531  ralv  2565  ceqsralt  2575  rspct  2643  rspc  2644  rspcimdv  2651  ralab  2695  ralab2  2699  ralrab2  2700  reu2  2723  reu6  2724  reu3  2725  rmo4  2728  reu8  2731  rmoim  2734  2reuswapdc  2737  2rmorex  2739  ra5  2840  rmo2ilem  2841  rmo3  2843  cbvralcsf  2902  dfss3  2929  dfss3f  2931  ssabral  3005  ss2rab  3010  rabss  3011  ssrab  3012  ralunb  3118  reuss2  3211  rabeq0  3241  rabxmdc  3243  disj  3262  disj1  3264  r19.2m  3303  r19.3rm  3304  ralidm  3315  rgenm  3317  ralf0  3318  ralm  3319  ralsns  3399  unissb  3601  dfint2  3608  elint2  3613  elintrab  3618  ssintrab  3629  dfiin2g  3681  invdisj  3750  dftr5  3848  trint  3860  repizf2lem  3905  ordsucim  4192  ordunisuc2r  4205  setindel  4221  elirr  4224  en2lp  4232  tfi  4248  zfinf2  4255  peano2  4261  peano5  4264  find  4265  raliunxp  4420  dmopab3  4491  issref  4650  asymref  4653  dffun7  4871  funcnv  4903  funcnvuni  4911  fnres  4958  fnopabg  4965  rexrnmpt  5253  dffo3  5257  acexmidlem2  5452  fz1sbc  8688  cbvrald  9196  bdcint  9266  bdcriota  9272  bj-ssom  9324  peano5set  9328  findset  9333  bj-inf2vn  9358  bj-inf2vn2  9359  bj-findis  9363  alsconv  9377