Metamath Proof Explorer

Theorem dfafv23

Description: A definition of function value in terms of iota, analogous to dffv3 . (Contributed by AV, 6-Sep-2022)

Ref Expression
Assertion dfafv23 
|- ( F defAt A -> ( F '''' A ) = ( iota x x e. ( F " { A } ) ) )

Proof

Step Hyp Ref Expression
1 dfatafv2iota 
 |-  ( F defAt A -> ( F '''' A ) = ( iota x A F x ) )
2 dfdfat2 
 |-  ( F defAt A <-> ( A e. dom F /\ E! x A F x ) )
3 2 simplbi 
 |-  ( F defAt A -> A e. dom F )
4 elimasng 
 |-  ( ( A e. dom F /\ x e. _V ) -> ( x e. ( F " { A } ) <-> <. A , x >. e. F ) )
5 3 4 sylan 
 |-  ( ( F defAt A /\ x e. _V ) -> ( x e. ( F " { A } ) <-> <. A , x >. e. F ) )
6 df-br 
 |-  ( A F x <-> <. A , x >. e. F )
7 5 6 bitr4di 
 |-  ( ( F defAt A /\ x e. _V ) -> ( x e. ( F " { A } ) <-> A F x ) )
8 7 elvd 
 |-  ( F defAt A -> ( x e. ( F " { A } ) <-> A F x ) )
9 8 iotabidv 
 |-  ( F defAt A -> ( iota x x e. ( F " { A } ) ) = ( iota x A F x ) )
10 1 9 eqtr4d 
 |-  ( F defAt A -> ( F '''' A ) = ( iota x x e. ( F " { A } ) ) )