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	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝐶 ) = ( ℩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		f1ocnvdm	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝐶 ) ∈ 𝐴 )
2		f1ocnvfvb	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 ) )
3	2	3expa	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 ) )
4	3	an32s	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 ) )
5		eqcom	⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝐶 ) ↔ ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 )
6	4 5	bitr4di	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ 𝑥 = ( ◡ 𝐹 ‘ 𝐶 ) ) )
7	1 6	riota5	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( ℩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) = ( ◡ 𝐹 ‘ 𝐶 ) )
8	7	eqcomd	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝐶 ) = ( ℩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) )