Definition df-ral 2477

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 2472	. 2 wff A. x e. A ph
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2164	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1362	. 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  2482  rexnalim  2483  dfrex2dc  2485  ralbida  2488  ralbidv2  2496  ralbid2  2498  ralbii2  2504  r2alf  2511  hbral  2523  hbra1  2524  nfra1  2525  nfraldw  2526  nfraldxy  2527  nfraldya  2529  r3al  2538  alral  2539  rsp  2541  rgen  2547  rgen2a  2548  ralim  2553  ralimi2  2554  ralimdaa  2560  ralimdv2  2564  ralrimi  2565  r19.21t  2569  ralrimd  2572  r19.21bi  2582  rexim  2588  r19.23t  2601  r19.26m  2625  r19.32r  2640  rabid2  2671  rabbi  2672  raleqf  2686  cbvralfw  2716  cbvralf  2718  cbvralvw  2730  cbvraldva2  2733  ralv  2777  ceqsralt  2787  rspct  2857  rspc  2858  rspcimdv  2865  rspc2gv  2876  ralab  2920  ralab2  2924  ralrab2  2925  reu2  2948  reu6  2949  reu3  2950  rmo4  2953  reu8  2956  rmo3f  2957  rmoim  2961  2reuswapdc  2964  2rmorex  2966  ra5  3074  rmo2ilem  3075  rmo3  3077  cbvralcsf  3143  dfss3  3169  dfss3f  3171  ssabral  3250  ss2rab  3255  rabss  3256  ssrab  3257  dfdif3  3269  ralunb  3340  reuss2  3439  rabeq0  3476  rabxmdc  3478  disj  3495  disj1  3497  r19.2m  3533  r19.2mOLD  3534  r19.3rm  3535  ralidm  3547  ralf0  3549  ralm  3550  ralsnsg  3655  ralsns  3656  unissb  3865  dfint2  3872  elint2  3877  elintrab  3882  ssintrab  3893  dfiin2g  3945  invdisj  4023  dftr5  4130  trint  4142  repizf2lem  4190  ordsucim  4532  ordunisuc2r  4546  setindel  4570  elirr  4573  en2lp  4586  zfregfr  4606  tfi  4614  zfinf2  4621  peano2  4627  peano5  4630  find  4631  raliunxp  4803  dmopab3  4875  issref  5048  asymref  5051  dffun7  5281  funcnv  5315  funcnvuni  5323  fnres  5370  fnopabg  5377  rexrnmpt  5701  dffo3  5705  acexmidlem2  5915  nfixpxy  6771  pw1dc0el  6967  isomnimap  7196  ismkvmap  7213  iswomnimap  7225  fz1sbc  10162  nnwosdc  12176  isprm2  12255  istopg  14167  cbvrald  15280  decidr  15288  bdcint  15369  bdcriota  15375  bj-axempty  15385  bj-indind  15424  bj-ssom  15428  findset  15437  bj-nnord  15450  bj-inf2vn  15466  bj-inf2vn2  15467  bj-findis  15471  alsconv  15570