Definition df-ral 2453

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 2448	. 2 wff A. x e. A ph
5	2	cv 1347	. . . . 5 class x
6	5, 3	wcel 2141	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1346	. 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  2458  rexnalim  2459  dfrex2dc  2461  ralbida  2464  ralbidv2  2472  ralbid2  2474  ralbii2  2480  r2alf  2487  hbral  2499  hbra1  2500  nfra1  2501  nfraldw  2502  nfraldxy  2503  nfraldya  2505  r3al  2514  alral  2515  rsp  2517  rgen  2523  rgen2a  2524  ralim  2529  ralimi2  2530  ralimdaa  2536  ralimdv2  2540  ralrimi  2541  r19.21t  2545  ralrimd  2548  r19.21bi  2558  rexim  2564  r19.23t  2577  r19.26m  2601  r19.32r  2616  rabid2  2646  rabbi  2647  raleqf  2661  cbvralfw  2687  cbvralf  2689  cbvralvw  2700  cbvraldva2  2703  ralv  2747  ceqsralt  2757  rspct  2827  rspc  2828  rspcimdv  2835  rspc2gv  2846  ralab  2890  ralab2  2894  ralrab2  2895  reu2  2918  reu6  2919  reu3  2920  rmo4  2923  reu8  2926  rmo3f  2927  rmoim  2931  2reuswapdc  2934  2rmorex  2936  ra5  3043  rmo2ilem  3044  rmo3  3046  cbvralcsf  3111  dfss3  3137  dfss3f  3139  ssabral  3218  ss2rab  3223  rabss  3224  ssrab  3225  dfdif3  3237  ralunb  3308  reuss2  3407  rabeq0  3444  rabxmdc  3446  disj  3463  disj1  3465  r19.2m  3501  r19.2mOLD  3502  r19.3rm  3503  ralidm  3515  rgenm  3517  ralf0  3518  ralm  3519  ralsnsg  3620  ralsns  3621  unissb  3826  dfint2  3833  elint2  3838  elintrab  3843  ssintrab  3854  dfiin2g  3906  invdisj  3983  dftr5  4090  trint  4102  repizf2lem  4147  ordsucim  4484  ordunisuc2r  4498  setindel  4522  elirr  4525  en2lp  4538  zfregfr  4558  tfi  4566  zfinf2  4573  peano2  4579  peano5  4582  find  4583  raliunxp  4752  dmopab3  4824  issref  4993  asymref  4996  dffun7  5225  funcnv  5259  funcnvuni  5267  fnres  5314  fnopabg  5321  rexrnmpt  5639  dffo3  5643  acexmidlem2  5850  nfixpxy  6695  pw1dc0el  6889  isomnimap  7113  ismkvmap  7130  iswomnimap  7142  fz1sbc  10052  nnwosdc  11994  isprm2  12071  istopg  12791  cbvrald  13823  decidr  13831  bdcint  13912  bdcriota  13918  bj-axempty  13928  bj-indind  13967  bj-ssom  13971  findset  13980  bj-nnord  13993  bj-inf2vn  14009  bj-inf2vn2  14010  bj-findis  14014  alsconv  14109