Theorem eusv1

Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by NM, 14-Oct-2010)

	Ref	Expression
Assertion	eusv1	⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ↔ ∃ 𝑦 ∀ 𝑥 𝑦 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴 )
2		sp	⊢ ( ∀ 𝑥 𝑧 = 𝐴 → 𝑧 = 𝐴 )
3		eqtr3	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐴 ) → 𝑦 = 𝑧 )
4	1 2 3	syl2an	⊢ ( ( ∀ 𝑥 𝑦 = 𝐴 ∧ ∀ 𝑥 𝑧 = 𝐴 ) → 𝑦 = 𝑧 )
5	4	gen2	⊢ ∀ 𝑦 ∀ 𝑧 ( ( ∀ 𝑥 𝑦 = 𝐴 ∧ ∀ 𝑥 𝑧 = 𝐴 ) → 𝑦 = 𝑧 )
6		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝐴 ↔ 𝑧 = 𝐴 ) )
7	6	albidv	⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 𝑦 = 𝐴 ↔ ∀ 𝑥 𝑧 = 𝐴 ) )
8	7	eu4	⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ↔ ( ∃ 𝑦 ∀ 𝑥 𝑦 = 𝐴 ∧ ∀ 𝑦 ∀ 𝑧 ( ( ∀ 𝑥 𝑦 = 𝐴 ∧ ∀ 𝑥 𝑧 = 𝐴 ) → 𝑦 = 𝑧 ) ) )
9	5 8	mpbiran2	⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ↔ ∃ 𝑦 ∀ 𝑥 𝑦 = 𝐴 )