Metamath Proof Explorer

Theorem isoeq1

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

Ref Expression
Assertion isoeq1 ⊢ H = G → H Isom R , S A B ↔ G Isom R , S A B

Proof

Step Hyp Ref Expression
1 f1oeq1 ⊢ H = G → H : A ⟶ 1-1 onto B ↔ G : A ⟶ 1-1 onto B
2 fveq1 ⊢ H = G → H ⁡ x = G ⁡ x
3 fveq1 ⊢ H = G → H ⁡ y = G ⁡ y
4 2 3 breq12d ⊢ H = G → H ⁡ x S H ⁡ y ↔ G ⁡ x S G ⁡ y
5 4 bibi2d ⊢ H = G → x R y ↔ H ⁡ x S H ⁡ y ↔ x R y ↔ G ⁡ x S G ⁡ y
6 5 2ralbidv ⊢ H = G → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ ∀ x ∈ A ∀ y ∈ A x R y ↔ G ⁡ x S G ⁡ y
7 1 6 anbi12d ⊢ H = G → H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ G : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ G ⁡ x S G ⁡ y
8 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
9 df-isom ⊢ G Isom R , S A B ↔ G : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ G ⁡ x S G ⁡ y
10 7 8 9 3bitr4g ⊢ H = G → H Isom R , S A B ↔ G Isom R , S A B