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

Metamath Proof Explorer

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 ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )