Definition df-ral 2515

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 2510	. 2 wff A. x e. A ph
5	2	cv 1396	. . . . 5 class x
6	5, 3	wcel 2202	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1395	. 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  2520  rexnalim  2521  dfrex2dc  2523  ralbida  2526  ralbidv2  2534  ralbid2  2536  ralbii2  2542  r2alf  2549  hbral  2561  hbra1  2562  nfra1  2563  nfraldw  2564  nfraldxy  2565  nfraldya  2567  r3al  2576  alral  2577  rsp  2579  rgen  2585  rgen2a  2586  ralim  2591  ralimi2  2592  ralimdaa  2598  ralimdv2  2602  ralrimi  2603  r19.21t  2607  ralrimd  2610  r19.21bi  2620  rexim  2626  r19.23t  2640  r19.26m  2664  r19.32r  2679  rabid2  2710  rabbi  2711  raleqf  2726  cbvralfw  2756  cbvralf  2758  cbvralvw  2771  cbvraldva2  2774  ralv  2820  ceqsralt  2830  rspct  2903  rspc  2904  rspcimdv  2911  rspc2gv  2922  ralab  2966  ralab2  2970  ralrab2  2971  reu2  2994  reu6  2995  reu3  2996  rmo4  2999  reu8  3002  rmo3f  3003  rmoim  3007  2reuswapdc  3010  2rmorex  3012  ra5  3121  rmo2ilem  3122  rmo3  3124  cbvralcsf  3190  dfss3  3216  dfss3f  3219  ssabral  3298  ss2rab  3303  rabss  3304  ssrab  3305  dfdif3  3317  ralunb  3388  reuss2  3487  rabeq0  3524  rabxmdc  3526  disj  3543  disj1  3545  r19.2m  3581  r19.2mOLD  3582  r19.3rm  3583  ralidm  3595  ralf0  3597  ralm  3598  ralsnsg  3706  ralsns  3707  unissb  3923  dfint2  3930  elint2  3935  elintrab  3940  ssintrab  3951  dfiin2g  4003  invdisj  4081  dftr5  4190  trint  4202  repizf2lem  4251  ordsucim  4598  ordunisuc2r  4612  setindel  4636  elirr  4639  en2lp  4652  zfregfr  4672  tfi  4680  zfinf2  4687  peano2  4693  peano5  4696  find  4697  raliunxp  4871  dmopab3  4944  issref  5119  asymref  5122  dffun7  5353  funcnv  5391  funcnvuni  5399  fnres  5449  fnopabg  5456  rexrnmpt  5790  dffo3  5794  acexmidlem2  6015  nfixpxy  6886  pw1dc0el  7103  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  fz1sbc  10331  nnwosdc  12628  isprm2  12707  istopg  14742  cbvrald  16435  decidr  16443  bdcint  16523  bdcriota  16529  bj-axempty  16539  bj-indind  16578  bj-ssom  16582  findset  16591  bj-nnord  16604  bj-inf2vn  16620  bj-inf2vn2  16621  bj-findis  16625  alsconv  16746