# Metamath Proof Explorer

## Theorem dffv3

Description: A definition of function value in terms of iota. (Contributed by Scott Fenton, 19-Feb-2013)

Ref Expression
Assertion dffv3 ${⊢}{F}\left({A}\right)=\left(\iota {x}|{x}\in {F}\left[\left\{{A}\right\}\right]\right)$

### Proof

Step Hyp Ref Expression
1 elimasng ${⊢}\left({A}\in \mathrm{V}\wedge {x}\in \mathrm{V}\right)\to \left({x}\in {F}\left[\left\{{A}\right\}\right]↔⟨{A},{x}⟩\in {F}\right)$
2 df-br ${⊢}{A}{F}{x}↔⟨{A},{x}⟩\in {F}$
3 1 2 syl6bbr ${⊢}\left({A}\in \mathrm{V}\wedge {x}\in \mathrm{V}\right)\to \left({x}\in {F}\left[\left\{{A}\right\}\right]↔{A}{F}{x}\right)$
4 3 elvd ${⊢}{A}\in \mathrm{V}\to \left({x}\in {F}\left[\left\{{A}\right\}\right]↔{A}{F}{x}\right)$
5 4 iotabidv ${⊢}{A}\in \mathrm{V}\to \left(\iota {x}|{x}\in {F}\left[\left\{{A}\right\}\right]\right)=\left(\iota {x}|{A}{F}{x}\right)$
6 df-fv ${⊢}{F}\left({A}\right)=\left(\iota {x}|{A}{F}{x}\right)$
7 5 6 syl6reqr ${⊢}{A}\in \mathrm{V}\to {F}\left({A}\right)=\left(\iota {x}|{x}\in {F}\left[\left\{{A}\right\}\right]\right)$
8 fvprc ${⊢}¬{A}\in \mathrm{V}\to {F}\left({A}\right)=\varnothing$
9 snprc ${⊢}¬{A}\in \mathrm{V}↔\left\{{A}\right\}=\varnothing$
10 9 biimpi ${⊢}¬{A}\in \mathrm{V}\to \left\{{A}\right\}=\varnothing$
11 10 imaeq2d ${⊢}¬{A}\in \mathrm{V}\to {F}\left[\left\{{A}\right\}\right]={F}\left[\varnothing \right]$
12 ima0 ${⊢}{F}\left[\varnothing \right]=\varnothing$
13 11 12 syl6eq ${⊢}¬{A}\in \mathrm{V}\to {F}\left[\left\{{A}\right\}\right]=\varnothing$
14 13 eleq2d ${⊢}¬{A}\in \mathrm{V}\to \left({x}\in {F}\left[\left\{{A}\right\}\right]↔{x}\in \varnothing \right)$
15 14 iotabidv ${⊢}¬{A}\in \mathrm{V}\to \left(\iota {x}|{x}\in {F}\left[\left\{{A}\right\}\right]\right)=\left(\iota {x}|{x}\in \varnothing \right)$
16 noel ${⊢}¬{x}\in \varnothing$
17 16 nex ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \varnothing$
18 euex ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{x}\in \varnothing \to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \varnothing$
19 17 18 mto ${⊢}¬\exists !{x}\phantom{\rule{.4em}{0ex}}{x}\in \varnothing$
20 iotanul ${⊢}¬\exists !{x}\phantom{\rule{.4em}{0ex}}{x}\in \varnothing \to \left(\iota {x}|{x}\in \varnothing \right)=\varnothing$
21 19 20 ax-mp ${⊢}\left(\iota {x}|{x}\in \varnothing \right)=\varnothing$
22 15 21 syl6eq ${⊢}¬{A}\in \mathrm{V}\to \left(\iota {x}|{x}\in {F}\left[\left\{{A}\right\}\right]\right)=\varnothing$
23 8 22 eqtr4d ${⊢}¬{A}\in \mathrm{V}\to {F}\left({A}\right)=\left(\iota {x}|{x}\in {F}\left[\left\{{A}\right\}\right]\right)$
24 7 23 pm2.61i ${⊢}{F}\left({A}\right)=\left(\iota {x}|{x}\in {F}\left[\left\{{A}\right\}\right]\right)$