Definition df-ral 2490

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 2485	. 2 wff A. x e. A ph
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2177	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1371	. 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  2495  rexnalim  2496  dfrex2dc  2498  ralbida  2501  ralbidv2  2509  ralbid2  2511  ralbii2  2517  r2alf  2524  hbral  2536  hbra1  2537  nfra1  2538  nfraldw  2539  nfraldxy  2540  nfraldya  2542  r3al  2551  alral  2552  rsp  2554  rgen  2560  rgen2a  2561  ralim  2566  ralimi2  2567  ralimdaa  2573  ralimdv2  2577  ralrimi  2578  r19.21t  2582  ralrimd  2585  r19.21bi  2595  rexim  2601  r19.23t  2614  r19.26m  2638  r19.32r  2653  rabid2  2684  rabbi  2685  raleqf  2699  cbvralfw  2729  cbvralf  2731  cbvralvw  2743  cbvraldva2  2746  ralv  2791  ceqsralt  2801  rspct  2874  rspc  2875  rspcimdv  2882  rspc2gv  2893  ralab  2937  ralab2  2941  ralrab2  2942  reu2  2965  reu6  2966  reu3  2967  rmo4  2970  reu8  2973  rmo3f  2974  rmoim  2978  2reuswapdc  2981  2rmorex  2983  ra5  3091  rmo2ilem  3092  rmo3  3094  cbvralcsf  3160  dfss3  3186  dfss3f  3189  ssabral  3268  ss2rab  3273  rabss  3274  ssrab  3275  dfdif3  3287  ralunb  3358  reuss2  3457  rabeq0  3494  rabxmdc  3496  disj  3513  disj1  3515  r19.2m  3551  r19.2mOLD  3552  r19.3rm  3553  ralidm  3565  ralf0  3567  ralm  3568  ralsnsg  3675  ralsns  3676  unissb  3889  dfint2  3896  elint2  3901  elintrab  3906  ssintrab  3917  dfiin2g  3969  invdisj  4047  dftr5  4156  trint  4168  repizf2lem  4216  ordsucim  4561  ordunisuc2r  4575  setindel  4599  elirr  4602  en2lp  4615  zfregfr  4635  tfi  4643  zfinf2  4650  peano2  4656  peano5  4659  find  4660  raliunxp  4832  dmopab3  4905  issref  5079  asymref  5082  dffun7  5312  funcnv  5349  funcnvuni  5357  fnres  5407  fnopabg  5414  rexrnmpt  5741  dffo3  5745  acexmidlem2  5959  nfixpxy  6822  pw1dc0el  7029  isomnimap  7260  ismkvmap  7277  iswomnimap  7289  fz1sbc  10248  nnwosdc  12445  isprm2  12524  istopg  14556  cbvrald  15894  decidr  15902  bdcint  15982  bdcriota  15988  bj-axempty  15998  bj-indind  16037  bj-ssom  16041  findset  16050  bj-nnord  16063  bj-inf2vn  16079  bj-inf2vn2  16080  bj-findis  16084  alsconv  16191