Definition df-ral 2527

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 2522	. 2 wff A. x e. A ph
5	2	cv 1397	. . . . 5 class x
6	5, 3	wcel 2205	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1396	. 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  2532  rexnalim  2533  dfrex2dc  2535  ralbida  2538  ralbidv2  2546  ralbid2  2548  ralbii2  2554  r2alf  2561  hbral  2573  hbra1  2574  nfra1  2575  nfraldw  2576  nfraldxy  2577  nfraldya  2579  r3al  2588  alral  2589  rsp  2591  rgen  2597  rgen2a  2598  ralim  2603  ralimi2  2604  ralimdaa  2610  ralimdv2  2614  ralrimi  2615  r19.21t  2619  ralrimd  2622  r19.21bi  2632  rexim  2638  r19.23t  2652  r19.26m  2676  r19.32r  2691  rabid2  2723  rabbi  2724  raleqf  2739  cbvralfw  2769  cbvralf  2771  cbvralvw  2784  cbvraldva2  2787  ralv  2833  ceqsralt  2843  rspct  2916  rspc  2917  rspcimdv  2924  rspc2gv  2935  ralab  2979  ralab2  2983  ralrab2  2984  reu2  3007  reu6  3008  reu3  3009  rmo4  3012  reu8  3015  rmo3f  3016  rmoim  3020  2reuswapdc  3023  2rmorex  3025  ra5  3134  rmo2ilem  3135  rmo3  3137  cbvralcsf  3203  dfss3  3229  dfss3f  3232  ssabral  3311  ss2rab  3316  rabss  3317  ssrab  3318  dfdif3  3331  ralunb  3402  reuss2  3503  rabeq0  3540  rabxmdc  3542  disj  3559  disj1  3561  r19.2m  3598  r19.2mOLD  3599  r19.3rm  3600  ralidm  3612  ralf0  3614  ralm  3615  ralsnsg  3728  ralsns  3729  unissb  3946  dfint2  3953  elint2  3958  elintrab  3963  ssintrab  3974  dfiin2g  4026  invdisj  4104  dftr5  4213  trint  4225  repizf2lem  4276  ordsucim  4624  ordunisuc2r  4638  setindel  4662  elirr  4665  en2lp  4678  zfregfr  4698  tfi  4706  zfinf2  4713  peano2  4719  peano5  4722  find  4723  raliunxp  4898  dmopab3  4971  issref  5147  asymref  5150  dffun7  5381  funcnv  5419  funcnvuni  5427  fnres  5477  fnopabg  5484  rexrnmpt  5822  dffo3  5826  acexmidlem2  6049  nfixpxy  6954  pw1dc0el  7173  isomnimap  7430  ismkvmap  7447  iswomnimap  7459  fz1sbc  10434  nnwosdc  12739  isprm2  12818  istopg  14881  cbvrald  16577  decidr  16585  bdcint  16664  bdcriota  16670  bj-axempty  16680  bj-indind  16719  bj-ssom  16723  findset  16732  bj-nnord  16745  bj-inf2vn  16761  bj-inf2vn2  16762  bj-findis  16766  alsconv  16894