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	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( ( 𝐹 '''' 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		nfeu1	⊢ Ⅎ 𝑦 ∃! 𝑦 𝐴 𝐹 𝑦
2		nfv	⊢ Ⅎ 𝑦 𝐴 𝐹 ( 𝐹 '''' 𝐴 )
3		euex	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃ 𝑦 𝐴 𝐹 𝑦 )
4		tz6.12-1-afv2	⊢ ( ( 𝐴 𝐹 𝑦 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) → ( 𝐹 '''' 𝐴 ) = 𝑦 )
5	4	expcom	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( 𝐴 𝐹 𝑦 → ( 𝐹 '''' 𝐴 ) = 𝑦 ) )
6		breq2	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝑦 → ( 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ↔ 𝐴 𝐹 𝑦 ) )
7	6	biimprd	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝑦 → ( 𝐴 𝐹 𝑦 → 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) )
8	5 7	syli	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( 𝐴 𝐹 𝑦 → 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) )
9	1 2 3 8	exlimimdd	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) )
10	9 6	syl5ibcom	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( ( 𝐹 '''' 𝐴 ) = 𝑦 → 𝐴 𝐹 𝑦 ) )
11	10 5	impbid	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( ( 𝐹 '''' 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )