Metamath Proof Explorer

Theorem isoeq4

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

Ref Expression
Assertion isoeq4 ⊢A=C→HIsomR,SAB↔HIsomR,SCB

Proof

Step Hyp Ref Expression
1 f1oeq2 ⊢A=C→H:A⟶1-1 ontoB↔H:C⟶1-1 ontoB
2 raleq ⊢A=C→∀y∈AxRy↔H⁡xSH⁡y↔∀y∈CxRy↔H⁡xSH⁡y
3 2 raleqbi1dv ⊢A=C→∀x∈A∀y∈AxRy↔H⁡xSH⁡y↔∀x∈C∀y∈CxRy↔H⁡xSH⁡y
4 1 3 anbi12d ⊢A=C→H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y↔H:C⟶1-1 ontoB∧∀x∈C∀y∈CxRy↔H⁡xSH⁡y
5 df-isom ⊢HIsomR,SAB↔H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y
6 df-isom ⊢HIsomR,SCB↔H:C⟶1-1 ontoB∧∀x∈C∀y∈CxRy↔H⁡xSH⁡y
7 4 5 6 3bitr4g ⊢A=C→HIsomR,SAB↔HIsomR,SCB