Theorem brfullfun

Description: A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brfullfun.1	|- A e. _V
	brfullfun.2	|- B e. _V
Assertion	brfullfun	|- ( A FullFun F B <-> B = ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		brfullfun.1	|- A e. _V
2		brfullfun.2	|- B e. _V
3		eqcom	|- ( ( FullFun F ` A ) = B <-> B = ( FullFun F ` A ) )
4		fullfunfnv	|- FullFun F Fn _V
5		fnbrfvb	|- ( ( FullFun F Fn _V /\ A e. _V ) -> ( ( FullFun F ` A ) = B <-> A FullFun F B ) )
6	4 1 5	mp2an	|- ( ( FullFun F ` A ) = B <-> A FullFun F B )
7		fullfunfv	|- ( FullFun F ` A ) = ( F ` A )
8	7	eqeq2i	|- ( B = ( FullFun F ` A ) <-> B = ( F ` A ) )
9	3 6 8	3bitr3i	|- ( A FullFun F B <-> B = ( F ` A ) )