Definition df-ral 2513

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	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )

Detailed syntax breakdown of Definition df-ral

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wral 2508	. 2 wff A. x e. A ph
5	2	cv 1394	. . . . 5 class x
6	5, 3	wcel 2200	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1393	. 2 wff A. x ( x e. A -> ph )
9	4, 8	wb 105	1 wff ( A. x e. A ph <-> A. x ( x e. A -> ph ) )

This definition is referenced by:  ralnex  2518  rexnalim  2519  dfrex2dc  2521  ralbida  2524  ralbidv2  2532  ralbid2  2534  ralbii2  2540  r2alf  2547  hbral  2559  hbra1  2560  nfra1  2561  nfraldw  2562  nfraldxy  2563  nfraldya  2565  r3al  2574  alral  2575  rsp  2577  rgen  2583  rgen2a  2584  ralim  2589  ralimi2  2590  ralimdaa  2596  ralimdv2  2600  ralrimi  2601  r19.21t  2605  ralrimd  2608  r19.21bi  2618  rexim  2624  r19.23t  2638  r19.26m  2662  r19.32r  2677  rabid2  2708  rabbi  2709  raleqf  2724  cbvralfw  2754  cbvralf  2756  cbvralvw  2769  cbvraldva2  2772  ralv  2817  ceqsralt  2827  rspct  2900  rspc  2901  rspcimdv  2908  rspc2gv  2919  ralab  2963  ralab2  2967  ralrab2  2968  reu2  2991  reu6  2992  reu3  2993  rmo4  2996  reu8  2999  rmo3f  3000  rmoim  3004  2reuswapdc  3007  2rmorex  3009  ra5  3118  rmo2ilem  3119  rmo3  3121  cbvralcsf  3187  dfss3  3213  dfss3f  3216  ssabral  3295  ss2rab  3300  rabss  3301  ssrab  3302  dfdif3  3314  ralunb  3385  reuss2  3484  rabeq0  3521  rabxmdc  3523  disj  3540  disj1  3542  r19.2m  3578  r19.2mOLD  3579  r19.3rm  3580  ralidm  3592  ralf0  3594  ralm  3595  ralsnsg  3703  ralsns  3704  unissb  3917  dfint2  3924  elint2  3929  elintrab  3934  ssintrab  3945  dfiin2g  3997  invdisj  4075  dftr5  4184  trint  4196  repizf2lem  4244  ordsucim  4591  ordunisuc2r  4605  setindel  4629  elirr  4632  en2lp  4645  zfregfr  4665  tfi  4673  zfinf2  4680  peano2  4686  peano5  4689  find  4690  raliunxp  4862  dmopab3  4935  issref  5110  asymref  5113  dffun7  5344  funcnv  5381  funcnvuni  5389  fnres  5439  fnopabg  5446  rexrnmpt  5777  dffo3  5781  acexmidlem2  5997  nfixpxy  6862  pw1dc0el  7069  isomnimap  7300  ismkvmap  7317  iswomnimap  7329  fz1sbc  10288  nnwosdc  12555  isprm2  12634  istopg  14667  cbvrald  16110  decidr  16118  bdcint  16198  bdcriota  16204  bj-axempty  16214  bj-indind  16253  bj-ssom  16257  findset  16266  bj-nnord  16279  bj-inf2vn  16295  bj-inf2vn2  16296  bj-findis  16300  alsconv  16407