Definition df-ral 2360

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 2355	. 2 wff A. x e. A ph
5	2	cv 1286	. . . . 5 class x
6	5, 3	wcel 1436	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1285	. 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  2365  rexnalim  2366  dfrex2dc  2367  ralbida  2370  ralbidv2  2378  ralbii2  2384  r2alf  2391  hbral  2403  hbra1  2404  nfra1  2405  nfraldxy  2406  nfraldya  2408  r3al  2416  alral  2417  rsp  2419  rgen  2424  rgen2a  2425  ralim  2430  ralimi2  2431  ralimdaa  2436  ralimdv2  2439  ralrimi  2440  r19.21t  2444  ralrimd  2447  r19.21bi  2457  rexim  2463  r19.23t  2475  r19.26m  2496  r19.32r  2510  rabid2  2539  rabbi  2540  raleqf  2554  cbvralf  2580  cbvraldva2  2590  ralv  2630  ceqsralt  2640  rspct  2708  rspc  2709  rspcimdv  2716  rspc2gv  2725  ralab  2766  ralab2  2770  ralrab2  2771  reu2  2794  reu6  2795  reu3  2796  rmo4  2799  reu8  2802  rmoim  2805  2reuswapdc  2808  2rmorex  2810  ra5  2916  rmo2ilem  2917  rmo3  2919  cbvralcsf  2979  dfss3  3004  dfss3f  3006  ssabral  3081  ss2rab  3086  rabss  3087  ssrab  3088  dfdif3  3099  ralunb  3170  reuss2  3268  rabeq0  3301  rabxmdc  3303  disj  3319  disj1  3321  r19.2m  3356  r19.3rm  3357  ralidm  3369  rgenm  3371  ralf0  3372  ralm  3373  ralsnsg  3465  ralsns  3466  unissb  3668  dfint2  3675  elint2  3680  elintrab  3685  ssintrab  3696  dfiin2g  3748  invdisj  3817  dftr5  3916  trint  3928  repizf2lem  3973  ordsucim  4292  ordunisuc2r  4306  setindel  4329  elirr  4332  en2lp  4345  zfregfr  4364  tfi  4372  zfinf2  4379  peano2  4385  peano5  4388  find  4389  raliunxp  4547  dmopab3  4619  issref  4783  asymref  4786  dffun7  5009  funcnv  5042  funcnvuni  5050  fnres  5097  fnopabg  5104  rexrnmpt  5407  dffo3  5411  acexmidlem2  5612  isomnimap  6740  fz1sbc  9443  isprm2  11005  cbvrald  11157  decidr  11165  bdcint  11237  bdcriota  11243  bj-axempty  11253  bj-indind  11296  bj-ssom  11300  findset  11309  bj-nnord  11322  bj-inf2vn  11338  bj-inf2vn2  11339  bj-findis  11343  alsconv  11390