Definition df-ral 2480

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 2475	. 2 wff A. x e. A ph
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2167	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1362	. 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  2485  rexnalim  2486  dfrex2dc  2488  ralbida  2491  ralbidv2  2499  ralbid2  2501  ralbii2  2507  r2alf  2514  hbral  2526  hbra1  2527  nfra1  2528  nfraldw  2529  nfraldxy  2530  nfraldya  2532  r3al  2541  alral  2542  rsp  2544  rgen  2550  rgen2a  2551  ralim  2556  ralimi2  2557  ralimdaa  2563  ralimdv2  2567  ralrimi  2568  r19.21t  2572  ralrimd  2575  r19.21bi  2585  rexim  2591  r19.23t  2604  r19.26m  2628  r19.32r  2643  rabid2  2674  rabbi  2675  raleqf  2689  cbvralfw  2719  cbvralf  2721  cbvralvw  2733  cbvraldva2  2736  ralv  2780  ceqsralt  2790  rspct  2861  rspc  2862  rspcimdv  2869  rspc2gv  2880  ralab  2924  ralab2  2928  ralrab2  2929  reu2  2952  reu6  2953  reu3  2954  rmo4  2957  reu8  2960  rmo3f  2961  rmoim  2965  2reuswapdc  2968  2rmorex  2970  ra5  3078  rmo2ilem  3079  rmo3  3081  cbvralcsf  3147  dfss3  3173  dfss3f  3175  ssabral  3254  ss2rab  3259  rabss  3260  ssrab  3261  dfdif3  3273  ralunb  3344  reuss2  3443  rabeq0  3480  rabxmdc  3482  disj  3499  disj1  3501  r19.2m  3537  r19.2mOLD  3538  r19.3rm  3539  ralidm  3551  ralf0  3553  ralm  3554  ralsnsg  3659  ralsns  3660  unissb  3869  dfint2  3876  elint2  3881  elintrab  3886  ssintrab  3897  dfiin2g  3949  invdisj  4027  dftr5  4134  trint  4146  repizf2lem  4194  ordsucim  4536  ordunisuc2r  4550  setindel  4574  elirr  4577  en2lp  4590  zfregfr  4610  tfi  4618  zfinf2  4625  peano2  4631  peano5  4634  find  4635  raliunxp  4807  dmopab3  4879  issref  5052  asymref  5055  dffun7  5285  funcnv  5319  funcnvuni  5327  fnres  5374  fnopabg  5381  rexrnmpt  5705  dffo3  5709  acexmidlem2  5919  nfixpxy  6776  pw1dc0el  6972  isomnimap  7203  ismkvmap  7220  iswomnimap  7232  fz1sbc  10171  nnwosdc  12206  isprm2  12285  istopg  14235  cbvrald  15434  decidr  15442  bdcint  15523  bdcriota  15529  bj-axempty  15539  bj-indind  15578  bj-ssom  15582  findset  15591  bj-nnord  15604  bj-inf2vn  15620  bj-inf2vn2  15621  bj-findis  15625  alsconv  15724