Theorem hbeleq 1559

Description: If x is effectively bound in y e. A, then it is effectively bound in y = A.

Hypothesis

Ref	Expression
hbeleq.1	|- (y e. A -> A.x y e. A)

Assertion

Ref	Expression
hbeleq	|- (y = A -> A.x y = A)

Distinct variable groups:   x,y   y,A

Proof of Theorem hbeleq

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (z e. y -> A.x z e. y)
2		ax-17 968	. . 3 |- (y e. z -> A.x y e. z)
3		hbeleq.1	. . 3 |- (y e. A -> A.x y e. A)
4	2, 3	hbel 1558	. 2 |- (z e. A -> A.x z e. A)
5	1, 4	hbeq 1557	1 |- (y = A -> A.x y = A)

Syntax hints:   -> wi 3  A.wal 951   = wceq 953   e. wcel 955

This theorem is referenced by:  vtoclgf 1837  cla4gf 1851  eqvincf 1875  uniiunlem 2122  hbpr 2416  intab 2550  hbsuc 3030  zfrep6 3600  fvopab4gf 3766  fvopabgf 3772  fvopabnf 3773  oprabval4g 4016  mapxpen 4475  xpmapenlem1 4476  xpmapenlem4 4479  tz9.12lem3 4633  scott0 4689  cplem2 4693  ac6lem 4726  lble 5994  seq1lem1 6246  cbvsum 6924

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465

Copyright terms: Public domain