Theorem hbeq 1171

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 group(s):   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 1170	. . . 4 |- (w e. A -> A.x w e. A)
3		hbeq.2	. . . . 5 |- (z e. B -> A.x z e. B)
4	3	hblem 1170	. . . 4 |- (w e. B -> A.x w e. B)
5	2, 4	hbbi 705	. . 3 |- ((w e. A <-> w e. B) -> A.x(w e. A <-> w e. B))
6	5	hbal 700	. 2 |- (A.w(w e. A <-> w e. B) -> A.xA.w(w e. A <-> w e. B))
7		dfcleq 1098	. 2 |- (A = B <-> A.w(w e. A <-> w e. B))
8	7	bial 695	. 2 |- (A.x A = B <-> A.xA.w(w e. A <-> w e. B))
9	6, 7, 8	3imtr4 192	1 |- (A = B -> A.x A = B)

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672   = wceq 1091   e. wcel 1092

This theorem is referenced by:  hbel 1172  hbeleq 1173  raleqf 1321  rexeqf 1322  reueqf 1323  rabeqf 1345  hbsbcg 1445  zfrepclf 1477  moop2 1910  eusn 1913  euuni 1954  reuuni2 1956  hbfn 2720  hbfo 2787  hbfv 2837  fvopabgf 2874  fvopabnf 2875  fvopab2 2878  cleqfvf 2881  elrnopab 2884  abrexexlem2 2911  f1fvf 2917  hbrdg 2974  elrnoprab 3054  dom2d 3307  cardprc 3667

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-9 799  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org