Definition df-ral 2422

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 2417	. 2 wff A. x e. A ph
5	2	cv 1331	. . . . 5 class x
6	5, 3	wcel 1481	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1330	. 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  2427  rexnalim  2428  dfrex2dc  2429  ralbida  2432  ralbidv2  2440  ralbid2  2442  ralbii2  2448  r2alf  2455  hbral  2467  hbra1  2468  nfra1  2469  nfraldxy  2470  nfraldya  2472  r3al  2480  alral  2481  rsp  2483  rgen  2488  rgen2a  2489  ralim  2494  ralimi2  2495  ralimdaa  2501  ralimdv2  2505  ralrimi  2506  r19.21t  2510  ralrimd  2513  r19.21bi  2523  rexim  2529  r19.23t  2542  r19.26m  2566  r19.32r  2581  rabid2  2610  rabbi  2611  raleqf  2625  cbvralf  2651  cbvraldva2  2664  ralv  2706  ceqsralt  2716  rspct  2786  rspc  2787  rspcimdv  2794  rspc2gv  2805  ralab  2848  ralab2  2852  ralrab2  2853  reu2  2876  reu6  2877  reu3  2878  rmo4  2881  reu8  2884  rmo3f  2885  rmoim  2889  2reuswapdc  2892  2rmorex  2894  ra5  3001  rmo2ilem  3002  rmo3  3004  cbvralcsf  3067  dfss3  3092  dfss3f  3094  ssabral  3173  ss2rab  3178  rabss  3179  ssrab  3180  dfdif3  3191  ralunb  3262  reuss2  3361  rabeq0  3397  rabxmdc  3399  disj  3416  disj1  3418  r19.2m  3454  r19.2mOLD  3455  r19.3rm  3456  ralidm  3468  rgenm  3470  ralf0  3471  ralm  3472  ralsnsg  3568  ralsns  3569  unissb  3774  dfint2  3781  elint2  3786  elintrab  3791  ssintrab  3802  dfiin2g  3854  invdisj  3931  dftr5  4037  trint  4049  repizf2lem  4093  ordsucim  4424  ordunisuc2r  4438  setindel  4461  elirr  4464  en2lp  4477  zfregfr  4496  tfi  4504  zfinf2  4511  peano2  4517  peano5  4520  find  4521  raliunxp  4688  dmopab3  4760  issref  4929  asymref  4932  dffun7  5158  funcnv  5192  funcnvuni  5200  fnres  5247  fnopabg  5254  rexrnmpt  5571  dffo3  5575  acexmidlem2  5779  nfixpxy  6619  isomnimap  7017  ismkvmap  7036  iswomnimap  7048  fz1sbc  9907  isprm2  11834  istopg  12205  cbvrald  13166  decidr  13174  bdcint  13246  bdcriota  13252  bj-axempty  13262  bj-indind  13301  bj-ssom  13305  findset  13314  bj-nnord  13327  bj-inf2vn  13343  bj-inf2vn2  13344  bj-findis  13348  alsconv  13437