Metamath Proof Explorer

Theorem isoeq3

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

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

Proof

Step Hyp Ref Expression
1 breq ⊢ S = T → H ⁡ x S H ⁡ y ↔ H ⁡ x T H ⁡ y
2 1 bibi2d ⊢ S = T → x R y ↔ H ⁡ x S H ⁡ y ↔ x R y ↔ H ⁡ x T H ⁡ y
3 2 2ralbidv ⊢ S = T → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x T H ⁡ y
4 3 anbi2d ⊢ S = 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 R y ↔ H ⁡ x T 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 R , T A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x T H ⁡ y
7 4 5 6 3bitr4g ⊢ S = T → H Isom R , S A B ↔ H Isom R , T A B