Metamath Proof Explorer

Theorem isoeq4

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

Ref Expression
Assertion isoeq4 ⊢ A = C → H Isom R , S A B ↔ H Isom R , S C B

Proof

Step Hyp Ref Expression
1 f1oeq2 ⊢ A = C → H : A ⟶ 1-1 onto B ↔ H : C ⟶ 1-1 onto B
2 raleq ⊢ A = C → ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ ∀ y ∈ C x R y ↔ H ⁡ x S H ⁡ y
3 2 raleqbi1dv ⊢ A = C → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ ∀ x ∈ C ∀ y ∈ C x R y ↔ H ⁡ x S H ⁡ y
4 1 3 anbi12d ⊢ A = C → H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ H : C ⟶ 1-1 onto B ∧ ∀ x ∈ C ∀ y ∈ C x R y ↔ H ⁡ x S 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 , S C B ↔ H : C ⟶ 1-1 onto B ∧ ∀ x ∈ C ∀ y ∈ C x R y ↔ H ⁡ x S H ⁡ y
7 4 5 6 3bitr4g ⊢ A = C → H Isom R , S A B ↔ H Isom R , S C B