Definition df-ral 2440

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 2435	. 2 wff A. x e. A ph
5	2	cv 1334	. . . . 5 class x
6	5, 3	wcel 2128	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1333	. 2 wff A. x ( x e. A -> ph )
9	4, 8	wb 104	1 wff ( A. x e. A ph <-> A. x ( x e. A -> ph ) )

This definition is referenced by:  ralnex  2445  rexnalim  2446  dfrex2dc  2448  ralbida  2451  ralbidv2  2459  ralbid2  2461  ralbii2  2467  r2alf  2474  hbral  2486  hbra1  2487  nfra1  2488  nfraldw  2489  nfraldxy  2490  nfraldya  2492  r3al  2501  alral  2502  rsp  2504  rgen  2510  rgen2a  2511  ralim  2516  ralimi2  2517  ralimdaa  2523  ralimdv2  2527  ralrimi  2528  r19.21t  2532  ralrimd  2535  r19.21bi  2545  rexim  2551  r19.23t  2564  r19.26m  2588  r19.32r  2603  rabid2  2633  rabbi  2634  raleqf  2648  cbvralf  2674  cbvralvw  2684  cbvraldva2  2687  ralv  2729  ceqsralt  2739  rspct  2809  rspc  2810  rspcimdv  2817  rspc2gv  2828  ralab  2872  ralab2  2876  ralrab2  2877  reu2  2900  reu6  2901  reu3  2902  rmo4  2905  reu8  2908  rmo3f  2909  rmoim  2913  2reuswapdc  2916  2rmorex  2918  ra5  3025  rmo2ilem  3026  rmo3  3028  cbvralcsf  3093  dfss3  3118  dfss3f  3120  ssabral  3199  ss2rab  3204  rabss  3205  ssrab  3206  dfdif3  3217  ralunb  3288  reuss2  3387  rabeq0  3423  rabxmdc  3425  disj  3442  disj1  3444  r19.2m  3480  r19.2mOLD  3481  r19.3rm  3482  ralidm  3494  rgenm  3496  ralf0  3497  ralm  3498  ralsnsg  3597  ralsns  3598  unissb  3803  dfint2  3810  elint2  3815  elintrab  3820  ssintrab  3831  dfiin2g  3883  invdisj  3960  dftr5  4066  trint  4078  repizf2lem  4123  ordsucim  4460  ordunisuc2r  4474  setindel  4498  elirr  4501  en2lp  4514  zfregfr  4534  tfi  4542  zfinf2  4549  peano2  4555  peano5  4558  find  4559  raliunxp  4728  dmopab3  4800  issref  4969  asymref  4972  dffun7  5198  funcnv  5232  funcnvuni  5240  fnres  5287  fnopabg  5294  rexrnmpt  5611  dffo3  5615  acexmidlem2  5822  nfixpxy  6663  pw1dc0el  6857  isomnimap  7081  ismkvmap  7098  iswomnimap  7110  fz1sbc  9999  isprm2  11998  istopg  12439  cbvrald  13404  decidr  13412  bdcint  13494  bdcriota  13500  bj-axempty  13510  bj-indind  13549  bj-ssom  13553  findset  13562  bj-nnord  13575  bj-inf2vn  13591  bj-inf2vn2  13592  bj-findis  13596  alsconv  13690