Theorem inisegn0a

Description: The inverse image of a singleton subset of an image is non-empty. (Contributed by Zhi Wang, 7-Nov-2025)

	Ref	Expression
Assertion	inisegn0a	|- ( A e. ( F " B ) -> ( `' F " { A } ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		elimag	|- ( A e. ( F " B ) -> ( A e. ( F " B ) <-> E. x e. B x F A ) )
2	1	ibi	|- ( A e. ( F " B ) -> E. x e. B x F A )
3		vex	|- x e. _V
4	3	eliniseg	|- ( A e. ( F " B ) -> ( x e. ( `' F " { A } ) <-> x F A ) )
5		ne0i	|- ( x e. ( `' F " { A } ) -> ( `' F " { A } ) =/= (/) )
6	4 5	biimtrrdi	|- ( A e. ( F " B ) -> ( x F A -> ( `' F " { A } ) =/= (/) ) )
7	6	rexlimdvw	|- ( A e. ( F " B ) -> ( E. x e. B x F A -> ( `' F " { A } ) =/= (/) ) )
8	2 7	mpd	|- ( A e. ( F " B ) -> ( `' F " { A } ) =/= (/) )