Theorem elpreima

Description: Membership in the preimage of a class under a function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Sky Winter, 22-Oct-2026)

	Ref	Expression
Assertion	elpreima	|- ( F Fn A -> ( B e. ( `' F " C ) <-> ( B e. A /\ ( F ` B ) e. C ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnvimass	|- ( `' F " C ) C_ dom F
2	1	sseli	|- ( B e. ( `' F " C ) -> B e. dom F )
3		fndm	|- ( F Fn A -> dom F = A )
4	3	eleq2d	|- ( F Fn A -> ( B e. dom F <-> B e. A ) )
5	2 4	imbitrid	|- ( F Fn A -> ( B e. ( `' F " C ) -> B e. A ) )
6	5	pm4.71rd	|- ( F Fn A -> ( B e. ( `' F " C ) <-> ( B e. A /\ B e. ( `' F " C ) ) ) )
7		fvimacnv	|- ( ( Fun F /\ B e. dom F ) -> ( ( F ` B ) e. C <-> B e. ( `' F " C ) ) )
8	7	funfni	|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) e. C <-> B e. ( `' F " C ) ) )
9	8	pm5.32da	|- ( F Fn A -> ( ( B e. A /\ ( F ` B ) e. C ) <-> ( B e. A /\ B e. ( `' F " C ) ) ) )
10	6 9	bitr4d	|- ( F Fn A -> ( B e. ( `' F " C ) <-> ( B e. A /\ ( F ` B ) e. C ) ) )