Definition df-ral 2488

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 2483	. 2 wff A. x e. A ph
5	2	cv 1371	. . . . 5 class x
6	5, 3	wcel 2175	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1370	. 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  2493  rexnalim  2494  dfrex2dc  2496  ralbida  2499  ralbidv2  2507  ralbid2  2509  ralbii2  2515  r2alf  2522  hbral  2534  hbra1  2535  nfra1  2536  nfraldw  2537  nfraldxy  2538  nfraldya  2540  r3al  2549  alral  2550  rsp  2552  rgen  2558  rgen2a  2559  ralim  2564  ralimi2  2565  ralimdaa  2571  ralimdv2  2575  ralrimi  2576  r19.21t  2580  ralrimd  2583  r19.21bi  2593  rexim  2599  r19.23t  2612  r19.26m  2636  r19.32r  2651  rabid2  2682  rabbi  2683  raleqf  2697  cbvralfw  2727  cbvralf  2729  cbvralvw  2741  cbvraldva2  2744  ralv  2788  ceqsralt  2798  rspct  2869  rspc  2870  rspcimdv  2877  rspc2gv  2888  ralab  2932  ralab2  2936  ralrab2  2937  reu2  2960  reu6  2961  reu3  2962  rmo4  2965  reu8  2968  rmo3f  2969  rmoim  2973  2reuswapdc  2976  2rmorex  2978  ra5  3086  rmo2ilem  3087  rmo3  3089  cbvralcsf  3155  dfss3  3181  dfss3f  3184  ssabral  3263  ss2rab  3268  rabss  3269  ssrab  3270  dfdif3  3282  ralunb  3353  reuss2  3452  rabeq0  3489  rabxmdc  3491  disj  3508  disj1  3510  r19.2m  3546  r19.2mOLD  3547  r19.3rm  3548  ralidm  3560  ralf0  3562  ralm  3563  ralsnsg  3669  ralsns  3670  unissb  3879  dfint2  3886  elint2  3891  elintrab  3896  ssintrab  3907  dfiin2g  3959  invdisj  4037  dftr5  4144  trint  4156  repizf2lem  4204  ordsucim  4547  ordunisuc2r  4561  setindel  4585  elirr  4588  en2lp  4601  zfregfr  4621  tfi  4629  zfinf2  4636  peano2  4642  peano5  4645  find  4646  raliunxp  4818  dmopab3  4890  issref  5064  asymref  5067  dffun7  5297  funcnv  5334  funcnvuni  5342  fnres  5391  fnopabg  5398  rexrnmpt  5722  dffo3  5726  acexmidlem2  5940  nfixpxy  6803  pw1dc0el  7007  isomnimap  7238  ismkvmap  7255  iswomnimap  7267  fz1sbc  10217  nnwosdc  12302  isprm2  12381  istopg  14413  cbvrald  15657  decidr  15665  bdcint  15746  bdcriota  15752  bj-axempty  15762  bj-indind  15801  bj-ssom  15805  findset  15814  bj-nnord  15827  bj-inf2vn  15843  bj-inf2vn2  15844  bj-findis  15848  alsconv  15952