Metamath Proof Explorer

Theorem f1ocnvfv3

Description: Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion f1ocnvfv3 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B → F -1 ⁡ C = ι x ∈ A | F ⁡ x = C

Proof

Step Hyp Ref Expression
1 f1ocnvdm ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B → F -1 ⁡ C ∈ A
2 f1ocnvfvb ⊢ F : A ⟶ 1-1 onto B ∧ x ∈ A ∧ C ∈ B → F ⁡ x = C ↔ F -1 ⁡ C = x
3 2 3expa ⊢ F : A ⟶ 1-1 onto B ∧ x ∈ A ∧ C ∈ B → F ⁡ x = C ↔ F -1 ⁡ C = x
4 3 an32s ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B ∧ x ∈ A → F ⁡ x = C ↔ F -1 ⁡ C = x
5 eqcom ⊢ x = F -1 ⁡ C ↔ F -1 ⁡ C = x
6 4 5 bitr4di ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B ∧ x ∈ A → F ⁡ x = C ↔ x = F -1 ⁡ C
7 1 6 riota5 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B → ι x ∈ A | F ⁡ x = C = F -1 ⁡ C
8 7 eqcomd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B → F -1 ⁡ C = ι x ∈ A | F ⁡ x = C