Theorem f1preimaex

Description: If the image under a one-to-one function exists, then the corresponding preimage also exists. (Contributed by BTernaryTau, 21-Jun-2026)

	Ref	Expression
Assertion	f1preimaex	|- ( ( F : A -1-1-> B /\ C C_ A /\ ( F " C ) e. V ) -> C e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-f1	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
2	1	simprbi	|- ( F : A -1-1-> B -> Fun `' F )
3		funimaexg	|- ( ( Fun `' F /\ ( F " C ) e. V ) -> ( `' F " ( F " C ) ) e. _V )
4	2 3	sylan	|- ( ( F : A -1-1-> B /\ ( F " C ) e. V ) -> ( `' F " ( F " C ) ) e. _V )
5	4	3adant2	|- ( ( F : A -1-1-> B /\ C C_ A /\ ( F " C ) e. V ) -> ( `' F " ( F " C ) ) e. _V )
6		f1imacnv	|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( `' F " ( F " C ) ) = C )
7	6	eleq1d	|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( ( `' F " ( F " C ) ) e. _V <-> C e. _V ) )
8	7	3adant3	|- ( ( F : A -1-1-> B /\ C C_ A /\ ( F " C ) e. V ) -> ( ( `' F " ( F " C ) ) e. _V <-> C e. _V ) )
9	5 8	mpbid	|- ( ( F : A -1-1-> B /\ C C_ A /\ ( F " C ) e. V ) -> C e. _V )