Metamath Proof Explorer


Theorem tz6.12c-afv2

Description: Corollary of Theorem 6.12(1) of TakeutiZaring p. 27, analogous to tz6.12c . (Contributed by AV, 5-Sep-2022)

Ref Expression
Assertion tz6.12c-afv2 ∃!yAFyF''''A=yAFy

Proof

Step Hyp Ref Expression
1 nfeu1 y∃!yAFy
2 nfv yAFF''''A
3 euex ∃!yAFyyAFy
4 tz6.12-1-afv2 AFy∃!yAFyF''''A=y
5 4 expcom ∃!yAFyAFyF''''A=y
6 breq2 F''''A=yAFF''''AAFy
7 6 biimprd F''''A=yAFyAFF''''A
8 5 7 syli ∃!yAFyAFyAFF''''A
9 1 2 3 8 exlimimdd ∃!yAFyAFF''''A
10 9 6 syl5ibcom ∃!yAFyF''''A=yAFy
11 10 5 impbid ∃!yAFyF''''A=yAFy