This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) =/= (/) )