Definition df-ral 2285

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

This definition is referenced by:  ralnex  2290  rexnalim  2291  ralbida  2294  ralbidv2  2302  ralbii2  2308  r2alf  2315  hbral  2327  hbra1  2328  nfra1  2329  nfraldxy  2330  nfraldya  2332  r3al  2340  alral  2341  rsp  2343  rgen  2348  rgen2a  2349  ralim  2354  ralimi2  2355  ralimdaa  2360  ralimdv2  2363  ralrimi  2364  r19.21t  2368  ralrimd  2371  r19.21bi  2381  rexim  2387  r19.23t  2397  r19.26m  2418  r19.32r  2431  rabid2  2460  rabbi  2461  raleqf  2475  cbvralf  2501  cbvraldva2  2511  ralv  2544  ceqsralt  2554  rspct  2622  rspc  2623  rspcimdv  2630  ralab  2674  ralab2  2678  ralrab2  2679  reu2  2702  reu6  2703  reu3  2704  rmo4  2707  reu8  2710  rmoim  2713  2reuswapdc  2716  2rmorex  2718  ra5  2819  rmo2ilem  2820  rmo3  2822  cbvralcsf  2881  dfss3  2908  dfss3f  2910  ssabral  2984  ss2rab  2989  rabss  2990  ssrab  2991  ralunb  3097  reuss2  3190  rabeq0  3220  rabxmdc  3222  disj  3241  disj1  3243  r19.2m  3282  r19.3rmOLD  3283  r19.3rm  3285  ralidm  3296  rgenm  3298  ralf0  3299  ralm  3300  ralsns  3378  unissb  3580  dfint2  3587  elint2  3592  elintrab  3597  ssintrab  3608  dfiin2g  3660  invdisj  3729  dftr5  3827  trint  3839  repizf2lem  3884  ordsucim  4172  ordunisuc2r  4185  setindel  4201  elirr  4204  en2lp  4212  tfi  4228  zfinf2  4235  peano2  4241  peano5  4244  find  4245  raliunxp  4400  dmopab3  4471  issref  4630  asymref  4633  dffun7  4850  funcnv  4882  funcnvuni  4890  fnres  4937  fnopabg  4944  rexrnmpt  5231  dffo3  5235  acexmidlem2  5429  cbvrald  7173  bdcint  7243  bdcriota  7249  bj-ssom  7297  peano5set  7301  findset  7306  bj-inf2vn  7331  bj-inf2vn2  7332  bj-findis  7336  alsconv  7350