Definition df-ral 2473

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 2468	. 2 wff A. x e. A ph
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2160	. . . 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  2478  rexnalim  2479  dfrex2dc  2481  ralbida  2484  ralbidv2  2492  ralbid2  2494  ralbii2  2500  r2alf  2507  hbral  2519  hbra1  2520  nfra1  2521  nfraldw  2522  nfraldxy  2523  nfraldya  2525  r3al  2534  alral  2535  rsp  2537  rgen  2543  rgen2a  2544  ralim  2549  ralimi2  2550  ralimdaa  2556  ralimdv2  2560  ralrimi  2561  r19.21t  2565  ralrimd  2568  r19.21bi  2578  rexim  2584  r19.23t  2597  r19.26m  2621  r19.32r  2636  rabid2  2667  rabbi  2668  raleqf  2682  cbvralfw  2708  cbvralf  2710  cbvralvw  2722  cbvraldva2  2725  ralv  2769  ceqsralt  2779  rspct  2849  rspc  2850  rspcimdv  2857  rspc2gv  2868  ralab  2912  ralab2  2916  ralrab2  2917  reu2  2940  reu6  2941  reu3  2942  rmo4  2945  reu8  2948  rmo3f  2949  rmoim  2953  2reuswapdc  2956  2rmorex  2958  ra5  3066  rmo2ilem  3067  rmo3  3069  cbvralcsf  3134  dfss3  3160  dfss3f  3162  ssabral  3241  ss2rab  3246  rabss  3247  ssrab  3248  dfdif3  3260  ralunb  3331  reuss2  3430  rabeq0  3467  rabxmdc  3469  disj  3486  disj1  3488  r19.2m  3524  r19.2mOLD  3525  r19.3rm  3526  ralidm  3538  rgenm  3540  ralf0  3541  ralm  3542  ralsnsg  3644  ralsns  3645  unissb  3854  dfint2  3861  elint2  3866  elintrab  3871  ssintrab  3882  dfiin2g  3934  invdisj  4012  dftr5  4119  trint  4131  repizf2lem  4179  ordsucim  4517  ordunisuc2r  4531  setindel  4555  elirr  4558  en2lp  4571  zfregfr  4591  tfi  4599  zfinf2  4606  peano2  4612  peano5  4615  find  4616  raliunxp  4786  dmopab3  4858  issref  5029  asymref  5032  dffun7  5262  funcnv  5296  funcnvuni  5304  fnres  5351  fnopabg  5358  rexrnmpt  5680  dffo3  5684  acexmidlem2  5893  nfixpxy  6743  pw1dc0el  6939  isomnimap  7165  ismkvmap  7182  iswomnimap  7194  fz1sbc  10126  nnwosdc  12072  isprm2  12149  istopg  13956  cbvrald  14998  decidr  15006  bdcint  15087  bdcriota  15093  bj-axempty  15103  bj-indind  15142  bj-ssom  15146  findset  15155  bj-nnord  15168  bj-inf2vn  15184  bj-inf2vn2  15185  bj-findis  15189  alsconv  15287