Definition df-ral 2620

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 2615	. 2 wff A.x e. A ph
5	2	cv 1641	. . . . 5 class x
6	5, 3	wcel 1710	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff (x e. A -> ph)
8	7, 2	wal 1540	. 2 wff A.x(x e. A -> ph)
9	4, 8	wb 176	1 wff (A.x e. A ph <-> A.x(x e. A -> ph))

This definition is referenced by:  ralnex  2625  rexnal  2626  ralbida  2629  ralbidv2  2637  ralbii2  2643  r2alf  2650  hbral  2663  hbra1  2664  nfra1  2665  nfrald  2666  r3al  2672  alral  2673  rsp  2675  rgen  2680  rgen2a  2681  ralim  2686  ralimi2  2687  ralimdaa  2692  ralimdv2  2695  ralrimi  2696  r19.21t  2700  ralrimd  2703  r19.21bi  2713  r19.23t  2729  r19.26m  2750  ralcom2  2776  rabid2  2789  rabbi  2790  raleqf  2804  cbvralf  2830  cbvraldva2  2840  ralv  2873  ceqsralt  2883  rspct  2949  rspc  2950  rspcimdv  2957  ralab  2998  ralab2  3002  ralrab2  3003  reu2  3025  reu6  3026  reu3  3027  rmo4  3030  reu8  3033  rmoim  3036  2reuswap  3039  2reu5lem2  3043  2reu5lem3  3044  ra5  3131  rmo2  3132  rmo3  3134  cbvralcsf  3199  dfss3  3264  dfss3f  3266  ssabral  3338  ss2rab  3343  rabss  3344  ssrab  3345  ralunb  3445  reuss2  3536  disj  3592  disj1  3594  r19.2z  3640  r19.3rz  3642  r19.3rzv  3644  ralidm  3654  ralf0  3657  ralsns  3764  disj5  3891  unissb  3922  dfint2  3929  elint2  3934  elintrab  3939  ssintrab  3950  dfiin2g  4001  eqpw1  4163  pw111  4171  ssrelk  4212  eqrelk  4213  sikexlem  4296  insklem  4305  nnadjoin  4521  nnpweq  4524  tfinnn  4535  spfininduct  4541  raliunxp  4824  dmopab3  4918  dffun7  5134  funcnv  5157  funcnvuni  5162  fnres  5200  fnopabg  5206  eqfnfv  5393  dff3  5421  dffo3  5423  clos1induct  5881  frds  5936