Theorem fncnvima2

Description: Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fncnvima2	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		elpreima	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
2	1	eqabdv	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ 𝐵 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) } )
3		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) }
4	2 3	eqtr4di	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 } )