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 = ι x | x F A

Proof

Step Hyp Ref Expression
1 dfatafv2iota F defAt A F '''' A = ι x | A F x
2 dfdfat2 F defAt A A dom F ∃! x A F x
3 2 simplbi F defAt A A dom F
4 elimasng A dom F x V x F A A x F
5 3 4 sylan F defAt A x V x F A A x F
6 df-br A F x A x F
7 5 6 bitr4di F defAt A x V x F A A F x
8 7 elvd F defAt A x F A A F x
9 8 iotabidv F defAt A ι x | x F A = ι x | A F x
10 1 9 eqtr4d F defAt A F '''' A = ι x | x F A