Definition df-ral 2619

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 2614	. 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  2624  rexnal  2625  ralbida  2628  ralbidv2  2636  ralbii2  2642  r2alf  2649  hbral  2662  hbra1  2663  nfra1  2664  nfrald  2665  r3al  2671  alral  2672  rsp  2674  rgen  2679  rgen2a  2680  ralim  2685  ralimi2  2686  ralimdaa  2691  ralimdv2  2694  ralrimi  2695  r19.21t  2699  ralrimd  2702  r19.21bi  2712  r19.23t  2728  r19.26m  2749  ralcom2  2775  rabid2  2788  rabbi  2789  raleqf  2803  cbvralf  2829  cbvraldva2  2839  ralv  2872  ceqsralt  2882  rspct  2948  rspc  2949  rspcimdv  2956  ralab  2997  ralab2  3001  ralrab2  3002  reu2  3024  reu6  3025  reu3  3026  rmo4  3029  reu8  3032  rmoim  3035  2reuswap  3038  2reu5lem2  3042  2reu5lem3  3043  ra5  3130  rmo2  3131  rmo3  3133  cbvralcsf  3198  dfss3  3263  dfss3f  3265  ssabral  3337  ss2rab  3342  rabss  3343  ssrab  3344  ralunb  3444  reuss2  3535  disj  3591  disj1  3593  r19.2z  3639  r19.3rz  3641  r19.3rzv  3643  ralidm  3653  ralf0  3656  ralsns  3763  disj5  3890  unissb  3921  dfint2  3928  elint2  3933  elintrab  3938  ssintrab  3949  dfiin2g  4000  eqpw1  4162  pw111  4170  ssrelk  4211  eqrelk  4212  sikexlem  4295  insklem  4304  nnadjoin  4520  nnpweq  4523  tfinnn  4534  spfininduct  4540  raliunxp  4823  dmopab3  4917  dffun7  5133  funcnv  5156  funcnvuni  5161  fnres  5199  fnopabg  5205  eqfnfv  5392  dff3  5420  dffo3  5422  clos1induct  5880  frds  5935