Metamath Proof Explorer

Theorem isoeq5

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

Ref Expression
Assertion isoeq5 ⊢ B = C → H Isom R , S A B ↔ H Isom R , S A C

Proof

Step Hyp Ref Expression
1 f1oeq3 ⊢ B = C → H : A ⟶ 1-1 onto B ↔ H : A ⟶ 1-1 onto C
2 1 anbi1d ⊢ B = C → H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ H : A ⟶ 1-1 onto C ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
3 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
4 df-isom ⊢ H Isom R , S A C ↔ H : A ⟶ 1-1 onto C ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
5 2 3 4 3bitr4g ⊢ B = C → H Isom R , S A B ↔ H Isom R , S A C