Metamath Proof Explorer

Theorem funimass5

Description: A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007)

		Ref	Expression
	Assertion	funimass5	\|- ( ( Fun F /\ A C_ dom F ) -> ( A C_ ( `' F " B ) <-> A. x e. A ( F ` x ) e. B ) )

Step	Hyp	Ref	Expression
1		funimass3	\|- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )
2		funimass4	\|- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )
3	1 2	bitr3d	\|- ( ( Fun F /\ A C_ dom F ) -> ( A C_ ( `' F " B ) <-> A. x e. A ( F ` x ) e. B ) )

Step

Hyp

Ref

Expression

 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )

 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )

1 2

 |-  ( ( Fun F /\ A C_ dom F ) -> ( A C_ ( `' F " B ) <-> A. x e. A ( F ` x ) e. B ) )