Theorem tz6.12cOLD

Description: Obsolete version of tz6.12c as of 23-Dec-2024. (Contributed by NM, 30-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	tz6.12cOLD	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( ( 𝐹 ‘ 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )

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