Theorem hbeq 1562

Description: If x is effectively bound in A and B, it is effectively bound in A = B.

Hypotheses

Ref	Expression
hbeq.1	|- (y e. A -> A.x y e. A)
hbeq.2	|- (z e. B -> A.x z e. B)

Assertion

Ref	Expression
hbeq	|- (A = B -> A.x A = B)

Distinct variable groups:   y,A   z,B   x,y   x,z

Proof of Theorem hbeq

Step	Hyp	Ref	Expression
1		hbeq.1	. . . . 5 |- (y e. A -> A.x y e. A)
2	1	hblem 1561	. . . 4 |- (w e. A -> A.x w e. A)
3		hbeq.2	. . . . 5 |- (z e. B -> A.x z e. B)
4	3	hblem 1561	. . . 4 |- (w e. B -> A.x w e. B)
5	2, 4	hbbi 1008	. . 3 |- ((w e. A <-> w e. B) -> A.x(w e. A <-> w e. B))
6	5	hbal 1003	. 2 |- (A.w(w e. A <-> w e. B) -> A.xA.w(w e. A <-> w e. B))
7		dfcleq 1468	. 2 |- (A = B <-> A.w(w e. A <-> w e. B))
8	7	albii 997	. 2 |- (A.x A = B <-> A.xA.w(w e. A <-> w e. B))
9	6, 7, 8	3imtr4 219	1 |- (A = B -> A.x A = B)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 952   = wceq 954   e. wcel 956

This theorem is referenced by:  hbel 1563  hbeleq 1564  hbne 1641  raleq1f 1780  rexeq1f 1781  reueq1f 1782  rabeqf 1804  hbeqd 1909  hbsbc1g 1944  hbsbcg 1947  csbieb 2026  csbie2t 2029  eusn 2442  zfrepclf 2694  moop2 2796  euuni 2876  reuuni2f 2878  reusn 2887  csbima12g 3405  hbfn 3576  hbfo 3662  hbfv 3720  csbfv12g 3733  fvopab4gf 3772  fvopabgf 3778  fvopabnf 3779  fvopab2 3782  eqfnfvf 3789  elrnopabg 3791  abrexexlem2 3850  f1fvf 3866  hbrdg 3927  csboprg 3977  oprabval2gf 4017  elrnoprabg 4114  dom2d 4391  cardprc 4841  csbnegg 5344  hbsum1 6929  hbsum 6930  fsum1f 6953  fsump1f 6957  isumnn0nna 7151  infcvgaux1 7162  fsum0diag4 7204  tgval3t 7575  minvecdist 8529  cnlnadjlem5 9942  irredt 10259  fgsb 10480  fgsb2 10485

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain