Theorem fvelrnb

Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995)

	Ref	Expression
Assertion	fvelrnb	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
2	1	eleq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ) )
3		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
4		eleq1	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ∈ V ↔ 𝐵 ∈ V ) )
5	3 4	mpbii	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝐵 → 𝐵 ∈ V )
6	5	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 → 𝐵 ∈ V )
7		eqeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝐵 = ( 𝐹 ‘ 𝑥 ) ) )
8		eqcom	⊢ ( 𝐵 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝐵 )
9	7 8	bitrdi	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
10	9	rexbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
11	6 10	elab3	⊢ ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 )
12	2 11	bitrdi	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )