Theorem afvpcfv0

Description: If the value of the alternative function at an argument is the universe, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afvpcfv0	|- ( ( F ''' A ) = _V -> ( F ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		dfafv2	|- ( F ''' A ) = if ( F defAt A , ( F ` A ) , _V )
2	1	eqeq1i	|- ( ( F ''' A ) = _V <-> if ( F defAt A , ( F ` A ) , _V ) = _V )
3		eqcom	|- ( if ( F defAt A , ( F ` A ) , _V ) = _V <-> _V = if ( F defAt A , ( F ` A ) , _V ) )
4		eqif	|- ( _V = if ( F defAt A , ( F ` A ) , _V ) <-> ( ( F defAt A /\ _V = ( F ` A ) ) \/ ( -. F defAt A /\ _V = _V ) ) )
5	3 4	bitri	|- ( if ( F defAt A , ( F ` A ) , _V ) = _V <-> ( ( F defAt A /\ _V = ( F ` A ) ) \/ ( -. F defAt A /\ _V = _V ) ) )
6		fveqvfvv	|- ( ( F ` A ) = _V -> ( F ` A ) = (/) )
7	6	eqcoms	|- ( _V = ( F ` A ) -> ( F ` A ) = (/) )
8	7	adantl	|- ( ( F defAt A /\ _V = ( F ` A ) ) -> ( F ` A ) = (/) )
9		fvfundmfvn0	|- ( ( F ` A ) =/= (/) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )
10		df-dfat	|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
11	9 10	sylibr	|- ( ( F ` A ) =/= (/) -> F defAt A )
12	11	necon1bi	|- ( -. F defAt A -> ( F ` A ) = (/) )
13	12	adantr	|- ( ( -. F defAt A /\ _V = _V ) -> ( F ` A ) = (/) )
14	8 13	jaoi	|- ( ( ( F defAt A /\ _V = ( F ` A ) ) \/ ( -. F defAt A /\ _V = _V ) ) -> ( F ` A ) = (/) )
15	5 14	sylbi	|- ( if ( F defAt A , ( F ` A ) , _V ) = _V -> ( F ` A ) = (/) )
16	2 15	sylbi	|- ( ( F ''' A ) = _V -> ( F ` A ) = (/) )