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

Proof

Step	Hyp	Ref	Expression
1		nfeu1	⊢ Ⅎ 𝑦 ∃! 𝑦 𝐴 𝐹 𝑦
2		nfv	⊢ Ⅎ 𝑦 𝐴 𝐹 ( 𝐹 ‘ 𝐴 )
3		euex	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃ 𝑦 𝐴 𝐹 𝑦 )
4		tz6.12-1	⊢ ( ( 𝐴 𝐹 𝑦 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 )
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	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( ( 𝐹 ‘ 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )