Definition df-ral 2281

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 2276	. 2 wff ∀x ∈ A φ
5	2	cv 1223	. . . . 5 class x
6	5, 3	wcel 1367	. . . 4 wff x ∈ A
7	6, 1	wi 4	. . 3 wff (x ∈ A → φ)
8	7, 2	wal 1222	. 2 wff ∀x(x ∈ A → φ)
9	4, 8	wb 98	1 wff (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))

This definition is referenced by:  ralnex  2286  rexnalim  2287  ralbida  2290  ralbidv2  2298  ralbii2  2304  r2alf  2311  hbral  2323  hbra1  2324  nfra1  2325  nfraldxy  2326  nfraldya  2328  r3al  2336  alral  2337  rsp  2339  rgen  2344  rgen2a  2345  ralim  2350  ralimi2  2351  ralimdaa  2356  ralimdv2  2359  ralrimi  2360  r19.21t  2364  ralrimd  2367  r19.21bi  2377  rexim  2383  r19.23t  2393  r19.26m  2414  r19.32r  2427  rabid2  2456  rabbi  2457  raleqf  2471  cbvralf  2497  cbvraldva2  2507  ralv  2540  ceqsralt  2550  rspct  2618  rspc  2619  rspcimdv  2626  ralab  2670  ralab2  2674  ralrab2  2675  reu2  2698  reu6  2699  reu3  2700  rmo4  2703  reu8  2706  rmoim  2709  2reuswapdc  2712  2rmorex  2714  ra5  2815  rmo2ilem  2816  rmo3  2818  cbvralcsf  2877  dfss3  2904  dfss3f  2906  ssabral  2980  ss2rab  2985  rabss  2986  ssrab  2987  ralunb  3093  reuss2  3186  rabeq0  3216  rabxmdc  3218  disj  3237  disj1  3239  r19.2m  3278  r19.3rm  3279  ralidm  3290  rgenm  3292  ralf0  3293  ralm  3294  ralsns  3372  unissb  3574  dfint2  3581  elint2  3586  elintrab  3591  ssintrab  3602  dfiin2g  3654  invdisj  3723  dftr5  3821  trint  3833  repizf2lem  3878  ordsucim  4165  ordunisuc2r  4178  setindel  4194  elirr  4197  en2lp  4205  tfi  4221  zfinf2  4228  peano2  4234  peano5  4237  find  4238  raliunxp  4393  dmopab3  4464  issref  4623  asymref  4626  dffun7  4843  funcnv  4875  funcnvuni  4883  fnres  4930  fnopabg  4937  rexrnmpt  5224  dffo3  5228  acexmidlem2  5422  cbvrald  8264  bdcint  8334  bdcriota  8340  bj-ssom  8392  peano5set  8396  findset  8401  bj-inf2vn  8426  bj-inf2vn2  8427  bj-findis  8431  alsconv  8445