Theorem eusv4

Description: Two ways to express single-valuedness of a class expression B ( y ) . (Contributed by NM, 27-Oct-2010)

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

Proof

Step	Hyp	Ref	Expression
1		eusv4.1	⊢ 𝐵 ∈ V
2		reusv2lem3	⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
3	1	a1i	⊢ ( 𝑦 ∈ 𝐴 → 𝐵 ∈ V )
4	2 3	mprg	⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )