This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eusv2

Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by NM, 15-Oct-2010) (Proof shortened by Mario Carneiro, 18-Nov-2016)

		Ref	Expression
	Hypothesis	eusv2.1	⊢ 𝐴 ∈ V
	Assertion	eusv2	⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ↔ ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eusv2.1	⊢ 𝐴 ∈ V
2	1	eusv2nf	⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ↔ Ⅎ 𝑥 𝐴 )
3		eusvnfb	⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ↔ ( Ⅎ 𝑥 𝐴 ∧ 𝐴 ∈ V ) )
4	1 3	mpbiran2	⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ↔ Ⅎ 𝑥 𝐴 )
5	2 4	bitr4i	⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ↔ ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 )