isoeq1

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

		Ref	Expression
	Assertion	isoeq1	$⊢ H = G \to (H {Isom}_{R, S} (A, B) \leftrightarrow G {Isom}_{R, S} (A, B))$

Step	Hyp	Ref	Expression
1		f1oeq1	$⊢ H = G \to (H : A \underset{1-1 onto}{⟶} B \leftrightarrow G : A \underset{1-1 onto}{⟶} B)$
2		fveq1	$⊢ H = G \to H (x) = G (x)$
3		fveq1	$⊢ H = G \to H (y) = G (y)$
4	2 3	breq12d	$⊢ H = G \to (H (x) S H (y) \leftrightarrow G (x) S G (y))$
5	4	bibi2d	$⊢ H = G \to ((x R y \leftrightarrow H (x) S H (y)) \leftrightarrow (x R y \leftrightarrow G (x) S G (y)))$
6	5	2ralbidv	$⊢ H = G \to (\forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)) \leftrightarrow \forall x \in A \forall y \in A (x R y \leftrightarrow G (x) S G (y)))$
7	1 6	anbi12d	$⊢ H = G \to ((H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y))) \leftrightarrow (G : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow G (x) S G (y))))$
8		df-isom	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)))$
9		df-isom	$⊢ G {Isom}_{R, S} (A, B) \leftrightarrow (G : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow G (x) S G (y)))$
10	7 8 9	3bitr4g	$⊢ H = G \to (H {Isom}_{R, S} (A, B) \leftrightarrow G {Isom}_{R, S} (A, B))$

Metamath Proof Explorer