Metamath Proof Explorer

Theorem dfafv22

Description: Alternate definition of ( F '''' A ) using ( FA ) directly. (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion dfafv22 
|- ( F '''' A ) = if ( F defAt A , ( F ` A ) , ~P U. ran F )

Proof

Step Hyp Ref Expression
1 df-afv2 
 |-  ( F '''' A ) = if ( F defAt A , ( iota x A F x ) , ~P U. ran F )
2 df-fv 
 |-  ( F ` A ) = ( iota x A F x )
3 2 eqcomi 
 |-  ( iota x A F x ) = ( F ` A )
4 ifeq1 
 |-  ( ( iota x A F x ) = ( F ` A ) -> if ( F defAt A , ( iota x A F x ) , ~P U. ran F ) = if ( F defAt A , ( F ` A ) , ~P U. ran F ) )
5 3 4 ax-mp 
 |-  if ( F defAt A , ( iota x A F x ) , ~P U. ran F ) = if ( F defAt A , ( F ` A ) , ~P U. ran F )
6 1 5 eqtri 
 |-  ( F '''' A ) = if ( F defAt A , ( F ` A ) , ~P U. ran F )