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  2818  ceqsralt  2828  rspct  2901  rspc  2902  rspcimdv  2909  rspc2gv  2920  ralab  2964  ralab2  2968  ralrab2  2969  reu2  2992  reu6  2993  reu3  2994  rmo4  2997  reu8  3000  rmo3f  3001  rmoim  3005  2reuswapdc  3008  2rmorex  3010  ra5  3119  rmo2ilem  3120  rmo3  3122  cbvralcsf  3188  dfss3  3214  dfss3f  3217  ssabral  3296  ss2rab  3301  rabss  3302  ssrab  3303  dfdif3  3315  ralunb  3386  reuss2  3485  rabeq0  3522  rabxmdc  3524  disj  3541  disj1  3543  r19.2m  3579  r19.2mOLD  3580  r19.3rm  3581  ralidm  3593  ralf0  3595  ralm  3596  ralsnsg  3704  ralsns  3705  unissb  3921  dfint2  3928  elint2  3933  elintrab  3938  ssintrab  3949  dfiin2g  4001  invdisj  4079  dftr5  4188  trint  4200  repizf2lem  4249  ordsucim  4596  ordunisuc2r  4610  setindel  4634  elirr  4637  en2lp  4650  zfregfr  4670  tfi  4678  zfinf2  4685  peano2  4691  peano5  4694  find  4695  raliunxp  4869  dmopab3  4942  issref  5117  asymref  5120  dffun7  5351  funcnv  5388  funcnvuni  5396  fnres  5446  fnopabg  5453  rexrnmpt  5786  dffo3  5790  acexmidlem2  6010  nfixpxy  6881  pw1dc0el  7096  isomnimap  7327  ismkvmap  7344  iswomnimap  7356  fz1sbc  10321  nnwosdc  12600  isprm2  12679  istopg  14713  cbvrald  16320  decidr  16328  bdcint  16408  bdcriota  16414  bj-axempty  16424  bj-indind  16463  bj-ssom  16467  findset  16476  bj-nnord  16489  bj-inf2vn  16505  bj-inf2vn2  16506  bj-findis  16510  alsconv  16620