Theorem hbeleq 1543

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 1190	. 2 |- (z e. y -> A.x z e. y)
2		ax-17 1190	. . 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 1542	. 2 |- (z e. A -> A.x z e. A)
5	1, 4	hbeq 1541	1 |- (y = A -> A.x y = A)

Syntax hints:   -> wi 3  A.wal 950   = wceq 1099   e. wcel 1105

This theorem is referenced by:  vtoclgf 1821  cla4gf 1835  eqvincf 1856  uniiunlem 2103  hbpr 2397  intab 2528  hbsuc 3003  zfrep6 3554  fvopab4gf 3720  fvopabgf 3726  fvopabnf 3727  oprabval4g 3970  mapxpen 4427  xpmapenlem1 4428  xpmapenlem4 4431  tz9.12lem3 4585  scott0 4641  cplem2 4645  ac6lem 4678  lble 5945  seq1lem1 6197  cbvsum 6875

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-9 1102  ax-17 1190  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-cleq 1446  df-clel 1449

Copyright terms: Public domain