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\in F\left[B\right]\to F^{-1}\left[\left\{A\right\}\right]\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		elimag	$$⊢A\in F\left[B\right]\to \left(A\in F\left[B\right]\leftrightarrow \exists x\in BxFA\right)$$
2	1	ibi	$$⊢A\in F\left[B\right]\to \exists x\in BxFA$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	eliniseg	$$⊢A\in F\left[B\right]\to \left(x\in F^{-1}\left[\left\{A\right\}\right]\leftrightarrow xFA\right)$$
5		ne0i	$$⊢x\in F^{-1}\left[\left\{A\right\}\right]\to F^{-1}\left[\left\{A\right\}\right]\ne \varnothing$$
6	4 5	biimtrrdi	$$⊢A\in F\left[B\right]\to \left(xFA\to F^{-1}\left[\left\{A\right\}\right]\ne \varnothing \right)$$
7	6	rexlimdvw	$$⊢A\in F\left[B\right]\to \left(\exists x\in BxFA\to F^{-1}\left[\left\{A\right\}\right]\ne \varnothing \right)$$
8	2 7	mpd	$$⊢A\in F\left[B\right]\to F^{-1}\left[\left\{A\right\}\right]\ne \varnothing$$