Theorem hbeq 1565

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 1564	. . . 4 |- (w e. A -> A.x w e. A)
3		hbeq.2	. . . . 5 |- (z e. B -> A.x z e. B)
4	3	hblem 1564	. . . 4 |- (w e. B -> A.x w e. B)
5	2, 4	hbbi 1010	. . 3 |- ((w e. A <-> w e. B) -> A.x(w e. A <-> w e. B))
6	5	hbal 1005	. 2 |- (A.w(w e. A <-> w e. B) -> A.xA.w(w e. A <-> w e. B))
7		dfcleq 1470	. 2 |- (A = B <-> A.w(w e. A <-> w e. B))
8	7	albii 999	. 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 954   = wceq 956   e. wcel 958

This theorem is referenced by:  hbel 1566  hbeleq 1567  hbne 1644  raleq1f 1783  rexeq1f 1784  reueq1f 1785  rabeqf 1808  hbeqd 1913  hbsbc1g 1948  hbsbcg 1951  csbieb 2030  csbie2t 2033  eusn 2446  zfrepclf 2699  moop2 2801  euuni 2881  reuuni2f 2883  reusn 2892  csbima12g 3413  hbfn 3584  hbfo 3671  hbfv 3729  csbfv12g 3742  fvopab4gf 3781  fvopabgf 3787  fvopabnf 3788  fvopab2 3791  eqfnfvf 3798  elrnopabg 3800  abrexexlem2 3859  f1fvf 3875  hbrdg 3936  csboprg 3986  oprabval2gf 4026  elrnoprabg 4124  dom2d 4404  cardprc 4861  csbnegg 5364  hbsum1 6983  hbsum 6984  fsum1f 7007  fsump1f 7011  isumnn0nna 7208  infcvgaux1 7219  fsum0diag4 7261  tgval3t 7625  iscaunns 7944  minvecdist 8585  cnlnadjlem5 10004  irredt 10322  fgsb 10570  fgsbOLD 10571  fgsb2 10580

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain