Theorem elmptima

Description: The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	elmptima	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ 𝐷 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) 𝐶 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		mptima	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ 𝐷 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 )
2	1	a1i	⊢ ( 𝐶 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ 𝐷 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 ) )
3	2	eleq2d	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ 𝐷 ) ↔ 𝐶 ∈ ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 ) ) )
4		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 )
5	4	elrnmpt	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) 𝐶 = 𝐵 ) )
6	3 5	bitrd	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ 𝐷 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) 𝐶 = 𝐵 ) )