Definition df-ral 2448

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 2443	. 2 wff A. x e. A ph
5	2	cv 1342	. . . . 5 class x
6	5, 3	wcel 2136	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1341	. 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  2453  rexnalim  2454  dfrex2dc  2456  ralbida  2459  ralbidv2  2467  ralbid2  2469  ralbii2  2475  r2alf  2482  hbral  2494  hbra1  2495  nfra1  2496  nfraldw  2497  nfraldxy  2498  nfraldya  2500  r3al  2509  alral  2510  rsp  2512  rgen  2518  rgen2a  2519  ralim  2524  ralimi2  2525  ralimdaa  2531  ralimdv2  2535  ralrimi  2536  r19.21t  2540  ralrimd  2543  r19.21bi  2553  rexim  2559  r19.23t  2572  r19.26m  2596  r19.32r  2611  rabid2  2641  rabbi  2642  raleqf  2656  cbvralfw  2682  cbvralf  2684  cbvralvw  2695  cbvraldva2  2698  ralv  2742  ceqsralt  2752  rspct  2822  rspc  2823  rspcimdv  2830  rspc2gv  2841  ralab  2885  ralab2  2889  ralrab2  2890  reu2  2913  reu6  2914  reu3  2915  rmo4  2918  reu8  2921  rmo3f  2922  rmoim  2926  2reuswapdc  2929  2rmorex  2931  ra5  3038  rmo2ilem  3039  rmo3  3041  cbvralcsf  3106  dfss3  3131  dfss3f  3133  ssabral  3212  ss2rab  3217  rabss  3218  ssrab  3219  dfdif3  3231  ralunb  3302  reuss2  3401  rabeq0  3437  rabxmdc  3439  disj  3456  disj1  3458  r19.2m  3494  r19.2mOLD  3495  r19.3rm  3496  ralidm  3508  rgenm  3510  ralf0  3511  ralm  3512  ralsnsg  3612  ralsns  3613  unissb  3818  dfint2  3825  elint2  3830  elintrab  3835  ssintrab  3846  dfiin2g  3898  invdisj  3975  dftr5  4082  trint  4094  repizf2lem  4139  ordsucim  4476  ordunisuc2r  4490  setindel  4514  elirr  4517  en2lp  4530  zfregfr  4550  tfi  4558  zfinf2  4565  peano2  4571  peano5  4574  find  4575  raliunxp  4744  dmopab3  4816  issref  4985  asymref  4988  dffun7  5214  funcnv  5248  funcnvuni  5256  fnres  5303  fnopabg  5310  rexrnmpt  5627  dffo3  5631  acexmidlem2  5838  nfixpxy  6679  pw1dc0el  6873  isomnimap  7097  ismkvmap  7114  iswomnimap  7126  fz1sbc  10027  nnwosdc  11968  isprm2  12045  istopg  12597  cbvrald  13629  decidr  13637  bdcint  13719  bdcriota  13725  bj-axempty  13735  bj-indind  13774  bj-ssom  13778  findset  13787  bj-nnord  13800  bj-inf2vn  13816  bj-inf2vn2  13817  bj-findis  13821  alsconv  13916