Theorem hbeq 1572

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

Hypotheses

Ref	Expression
hbeq.1	⊢ (y ∈ A → ∀x y ∈ A)
hbeq.2	⊢ (z ∈ B → ∀x z ∈ B)

Assertion

Ref	Expression
hbeq	⊢ (A = B → ∀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 ∈ A → ∀x y ∈ A)
2	1	hblem 1571	. . . 4 ⊢ (w ∈ A → ∀x w ∈ A)
3		hbeq.2	. . . . 5 ⊢ (z ∈ B → ∀x z ∈ B)
4	3	hblem 1571	. . . 4 ⊢ (w ∈ B → ∀x w ∈ B)
5	2, 4	hbbi 1016	. . 3 ⊢ ((w ∈ A ↔ w ∈ B) → ∀x(w ∈ A ↔ w ∈ B))
6	5	hbal 1011	. 2 ⊢ (∀w(w ∈ A ↔ w ∈ B) → ∀x∀w(w ∈ A ↔ w ∈ B))
7		dfcleq 1477	. 2 ⊢ (A = B ↔ ∀w(w ∈ A ↔ w ∈ B))
8	7	albii 1005	. 2 ⊢ (∀x A = B ↔ ∀x∀w(w ∈ A ↔ w ∈ B))
9	6, 7, 8	3imtr4 219	1 ⊢ (A = B → ∀x A = B)

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 958   = wceq 960   ∈ wcel 962

This theorem is referenced by:  hbel 1573  hbeleq 1574  hbne 1651  raleq1f 1790  rexeq1f 1791  reueq1f 1792  rabeqf 1815  hbeqd 1920  hbsbc1g 1955  hbsbcg 1958  csbieb 2039  csbie2t 2042  eusn 2456  zfrepclf 2712  moop2 2815  euuni 2895  reuuni2f 2897  reusn 2906  csbima12g 3427  hbfn 3598  hbfo 3685  hbfv 3743  csbfv12g 3756  fvopab4gf 3795  fvopabgf 3801  fvopabnf 3802  fvopab2 3805  eqfnfvf 3812  elrnopabg 3814  abrexexlem2 3873  f1fvf 3889  hbrdg 3950  csboprg 4000  oprabval2gf 4040  elrnoprabg 4138  dom2d 4418  cardprc 4874  csbnegg 5377  hbsum1 6997  hbsum 6998  fsum1f 7021  fsump1f 7025  isumnn0nna 7222  infcvgaux1 7233  fsum0diag4 7275  tgval3t 7637  iscaunns 7953  minvecdist 8593  cnlnadjlem5 10011  irredt 10330  fgsb 10575  fgsb2 10580

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-ext 1466

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 985  df-cleq 1476  df-clel 1479

Copyright terms: Public domain