# Metamath Proof Explorer

## Theorem isoeq2

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

Ref Expression
Assertion isoeq2 ${⊢}{R}={T}\to \left({H}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{T},{S}}\left({A},{B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 breq ${⊢}{R}={T}\to \left({x}{R}{y}↔{x}{T}{y}\right)$
2 1 bibi1d ${⊢}{R}={T}\to \left(\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\left({x}{T}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)$
3 2 2ralbidv ${⊢}{R}={T}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{T}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)$
4 3 anbi2d ${⊢}{R}={T}\to \left(\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{T}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)\right)$
5 df-isom ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)$
6 df-isom ${⊢}{H}{Isom}_{{T},{S}}\left({A},{B}\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{T}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)$
7 4 5 6 3bitr4g ${⊢}{R}={T}\to \left({H}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{T},{S}}\left({A},{B}\right)\right)$