Definition df-ral 2353

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 2348	. 2 wff A. x e. A ph
5	2	cv 1283	. . . . 5 class x
6	5, 3	wcel 1433	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1282	. 2 wff A. x ( x e. A -> ph )
9	4, 8	wb 103	1 wff ( A. x e. A ph <-> A. x ( x e. A -> ph ) )

This definition is referenced by:  ralnex  2358  rexnalim  2359  ralbida  2362  ralbidv2  2370  ralbii2  2376  r2alf  2383  hbral  2395  hbra1  2396  nfra1  2397  nfraldxy  2398  nfraldya  2400  r3al  2408  alral  2409  rsp  2411  rgen  2416  rgen2a  2417  ralim  2422  ralimi2  2423  ralimdaa  2428  ralimdv2  2431  ralrimi  2432  r19.21t  2436  ralrimd  2439  r19.21bi  2449  rexim  2455  r19.23t  2467  r19.26m  2488  r19.32r  2501  rabid2  2530  rabbi  2531  raleqf  2545  cbvralf  2571  cbvraldva2  2581  ralv  2616  ceqsralt  2626  rspct  2694  rspc  2695  rspcimdv  2702  rspc2gv  2712  ralab  2752  ralab2  2756  ralrab2  2757  reu2  2780  reu6  2781  reu3  2782  rmo4  2785  reu8  2788  rmoim  2791  2reuswapdc  2794  2rmorex  2796  ra5  2902  rmo2ilem  2903  rmo3  2905  cbvralcsf  2964  dfss3  2989  dfss3f  2991  ssabral  3065  ss2rab  3070  rabss  3071  ssrab  3072  ralunb  3153  reuss2  3244  rabeq0  3274  rabxmdc  3276  disj  3292  disj1  3294  r19.2m  3329  r19.3rm  3330  ralidm  3341  rgenm  3343  ralf0  3344  ralm  3345  ralsnsg  3430  ralsns  3431  unissb  3631  dfint2  3638  elint2  3643  elintrab  3648  ssintrab  3659  dfiin2g  3711  invdisj  3780  dftr5  3878  trint  3890  repizf2lem  3935  ordsucim  4244  ordunisuc2r  4258  setindel  4281  elirr  4284  en2lp  4297  zfregfr  4316  tfi  4323  zfinf2  4330  peano2  4336  peano5  4339  find  4340  raliunxp  4495  dmopab3  4566  issref  4727  asymref  4730  dffun7  4948  funcnv  4980  funcnvuni  4988  fnres  5035  fnopabg  5042  rexrnmpt  5331  dffo3  5335  acexmidlem2  5529  fz1sbc  9113  isprm2  10499  cbvrald  10598  bdcint  10668  bdcriota  10674  bj-axempty  10684  bj-indind  10727  bj-ssom  10731  findset  10740  bj-nnord  10753  bj-inf2vn  10769  bj-inf2vn2  10770  bj-findis  10774  alsconv  10791