Theorem elpreimad

Description: Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	elpreimad.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	elpreimad.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	elpreimad.c	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 )
Assertion	elpreimad	⊢ ( 𝜑 → 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elpreimad.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		elpreimad.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		elpreimad.c	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 )
4		elpreima	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) ) )
6	2 3 5	mpbir2and	⊢ ( 𝜑 → 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) )