This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1ocnvfv

Description: Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004)

Ref Expression
Assertion f1ocnvfv ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F ⁡ C = D → F -1 ⁡ D = C

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ D = F ⁡ C → F -1 ⁡ D = F -1 ⁡ F ⁡ C
2 1 eqcoms ⊢ F ⁡ C = D → F -1 ⁡ D = F -1 ⁡ F ⁡ C
3 f1ocnvfv1 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F -1 ⁡ F ⁡ C = C
4 3 eqeq2d ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F -1 ⁡ D = F -1 ⁡ F ⁡ C ↔ F -1 ⁡ D = C
5 2 4 imbitrid ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F ⁡ C = D → F -1 ⁡ D = C