Theorem dfafv2

Description: Alternative definition of ( F ''' A ) using ( FA ) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017) (Revised by AV, 25-Aug-2022)

	Ref	Expression
Assertion	dfafv2	|- ( F ''' A ) = if ( F defAt A , ( F ` A ) , _V )

Proof

Step	Hyp	Ref	Expression
1		df-fv	|- ( F ` A ) = ( iota x A F x )
2		simprr	|- ( ( T. /\ ( A e. dom F /\ E! x A F x ) ) -> E! x A F x )
3		reuaiotaiota	|- ( E! x A F x <-> ( iota x A F x ) = ( iota' x A F x ) )
4	2 3	sylib	|- ( ( T. /\ ( A e. dom F /\ E! x A F x ) ) -> ( iota x A F x ) = ( iota' x A F x ) )
5	1 4	eqtrid	|- ( ( T. /\ ( A e. dom F /\ E! x A F x ) ) -> ( F ` A ) = ( iota' x A F x ) )
6		eubrdm	|- ( E! x A F x -> A e. dom F )
7	6	ancri	|- ( E! x A F x -> ( A e. dom F /\ E! x A F x ) )
8	7	con3i	|- ( -. ( A e. dom F /\ E! x A F x ) -> -. E! x A F x )
9	8	adantl	|- ( ( T. /\ -. ( A e. dom F /\ E! x A F x ) ) -> -. E! x A F x )
10		aiotavb	|- ( -. E! x A F x <-> ( iota' x A F x ) = _V )
11	9 10	sylib	|- ( ( T. /\ -. ( A e. dom F /\ E! x A F x ) ) -> ( iota' x A F x ) = _V )
12	11	eqcomd	|- ( ( T. /\ -. ( A e. dom F /\ E! x A F x ) ) -> _V = ( iota' x A F x ) )
13	5 12	ifeqda	|- ( T. -> if ( ( A e. dom F /\ E! x A F x ) , ( F ` A ) , _V ) = ( iota' x A F x ) )
14	13	mptru	|- if ( ( A e. dom F /\ E! x A F x ) , ( F ` A ) , _V ) = ( iota' x A F x )
15		dfdfat2	|- ( F defAt A <-> ( A e. dom F /\ E! x A F x ) )
16		ifbi	|- ( ( F defAt A <-> ( A e. dom F /\ E! x A F x ) ) -> if ( F defAt A , ( F ` A ) , _V ) = if ( ( A e. dom F /\ E! x A F x ) , ( F ` A ) , _V ) )
17	15 16	ax-mp	|- if ( F defAt A , ( F ` A ) , _V ) = if ( ( A e. dom F /\ E! x A F x ) , ( F ` A ) , _V )
18		df-afv	|- ( F ''' A ) = ( iota' x A F x )
19	14 17 18	3eqtr4ri	|- ( F ''' A ) = if ( F defAt A , ( F ` A ) , _V )