Definition df-ral 2358

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 2353	. 2 wff A. x e. A ph
5	2	cv 1284	. . . . 5 class x
6	5, 3	wcel 1434	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1283	. 2 wff A. x ( x e. A -> ph )
9	4, 8	wb 103	1 wff ( A. x e. A ph <-> A. x ( x e. A -> ph ) )

This definition is referenced by:  ralnex  2363  rexnalim  2364  dfrex2dc  2365  ralbida  2368  ralbidv2  2376  ralbii2  2382  r2alf  2389  hbral  2401  hbra1  2402  nfra1  2403  nfraldxy  2404  nfraldya  2406  r3al  2414  alral  2415  rsp  2417  rgen  2422  rgen2a  2423  ralim  2428  ralimi2  2429  ralimdaa  2434  ralimdv2  2437  ralrimi  2438  r19.21t  2442  ralrimd  2445  r19.21bi  2455  rexim  2461  r19.23t  2473  r19.26m  2494  r19.32r  2507  rabid2  2536  rabbi  2537  raleqf  2551  cbvralf  2577  cbvraldva2  2587  ralv  2627  ceqsralt  2637  rspct  2705  rspc  2706  rspcimdv  2713  rspc2gv  2722  ralab  2763  ralab2  2767  ralrab2  2768  reu2  2791  reu6  2792  reu3  2793  rmo4  2796  reu8  2799  rmoim  2802  2reuswapdc  2805  2rmorex  2807  ra5  2913  rmo2ilem  2914  rmo3  2916  cbvralcsf  2975  dfss3  3000  dfss3f  3002  ssabral  3076  ss2rab  3081  rabss  3082  ssrab  3083  dfdif3  3094  ralunb  3165  reuss2  3262  rabeq0  3295  rabxmdc  3297  disj  3313  disj1  3315  r19.2m  3350  r19.3rm  3351  ralidm  3363  rgenm  3365  ralf0  3366  ralm  3367  ralsnsg  3454  ralsns  3455  unissb  3657  dfint2  3664  elint2  3669  elintrab  3674  ssintrab  3685  dfiin2g  3737  invdisj  3806  dftr5  3904  trint  3916  repizf2lem  3961  ordsucim  4279  ordunisuc2r  4293  setindel  4316  elirr  4319  en2lp  4332  zfregfr  4351  tfi  4359  zfinf2  4366  peano2  4372  peano5  4375  find  4376  raliunxp  4534  dmopab3  4606  issref  4768  asymref  4771  dffun7  4994  funcnv  5027  funcnvuni  5035  fnres  5082  fnopabg  5089  rexrnmpt  5386  dffo3  5390  acexmidlem2  5587  isomnimap  6697  fz1sbc  9402  isprm2  10878  cbvrald  11030  decidr  11038  bdcint  11110  bdcriota  11116  bj-axempty  11126  bj-indind  11169  bj-ssom  11173  findset  11182  bj-nnord  11195  bj-inf2vn  11211  bj-inf2vn2  11212  bj-findis  11216  alsconv  11233