Theorem afvelrnb

Description: A member of a function's range is a value of the function, analogous to fvelrnb with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afvelrnb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) = 𝐵 ) )

Proof

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