# Metamath Proof Explorer

## Theorem tz6.12c

Description: Corollary of Theorem 6.12(1) of TakeutiZaring p. 27. (Contributed by NM, 30-Apr-2004)

Ref Expression
Assertion tz6.12c ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to \left({F}\left({A}\right)={y}↔{A}{F}{y}\right)$

### Proof

Step Hyp Ref Expression
1 nfeu1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$
2 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{A}{F}{F}\left({A}\right)$
3 euex ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to \exists {y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$
4 tz6.12-1 ${⊢}\left({A}{F}{y}\wedge \exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)\to {F}\left({A}\right)={y}$
5 4 expcom ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to \left({A}{F}{y}\to {F}\left({A}\right)={y}\right)$
6 breq2 ${⊢}{F}\left({A}\right)={y}\to \left({A}{F}{F}\left({A}\right)↔{A}{F}{y}\right)$
7 6 biimprd ${⊢}{F}\left({A}\right)={y}\to \left({A}{F}{y}\to {A}{F}{F}\left({A}\right)\right)$
8 5 7 syli ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to \left({A}{F}{y}\to {A}{F}{F}\left({A}\right)\right)$
9 1 2 3 8 exlimimdd ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to {A}{F}{F}\left({A}\right)$
10 9 6 syl5ibcom ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to \left({F}\left({A}\right)={y}\to {A}{F}{y}\right)$
11 10 5 impbid ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to \left({F}\left({A}\right)={y}↔{A}{F}{y}\right)$