Metamath Proof Explorer

Theorem isoeq2

Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004)

Ref Expression
Assertion isoeq2 ⊢ R = T → H Isom R , S A B ↔ H Isom T , S A B

Proof

Step Hyp Ref Expression
1 breq ⊢ R = T → x R y ↔ x T y
2 1 bibi1d ⊢ R = T → x R y ↔ H ⁡ x S H ⁡ y ↔ x T y ↔ H ⁡ x S H ⁡ y
3 2 2ralbidv ⊢ R = T → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ ∀ x ∈ A ∀ y ∈ A x T y ↔ H ⁡ x S H ⁡ y
4 3 anbi2d ⊢ R = T → H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x T y ↔ H ⁡ x S H ⁡ y
5 df-isom ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
6 df-isom ⊢ H Isom T , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x T y ↔ H ⁡ x S H ⁡ y
7 4 5 6 3bitr4g ⊢ R = T → H Isom R , S A B ↔ H Isom T , S A B