Theorem afvelrnb0

Description: A member of a function's range is a value of the function, only one direction of implication of fvelrnb . (Contributed by Alexander van der Vekens, 1-Jun-2017)

	Ref	Expression
Assertion	afvelrnb0	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fnrnafv	⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) } )
2	1	eleq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) } ) )
3		eqeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ( 𝐹 ''' 𝑥 ) ↔ 𝐵 = ( 𝐹 ''' 𝑥 ) ) )
4		eqcom	⊢ ( 𝐵 = ( 𝐹 ''' 𝑥 ) ↔ ( 𝐹 ''' 𝑥 ) = 𝐵 )
5	3 4	bitrdi	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ( 𝐹 ''' 𝑥 ) ↔ ( 𝐹 ''' 𝑥 ) = 𝐵 ) )
6	5	rexbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) = 𝐵 ) )
7	6	elabg	⊢ ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) } → ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) } ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) = 𝐵 ) )
8	7	ibi	⊢ ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) } → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) = 𝐵 )
9	2 8	biimtrdi	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) = 𝐵 ) )