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

Metamath Proof Explorer

Theorem moop2

Description: "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypothesis moop2.1 ⊢ 𝐵 ∈ V
Assertion moop2 ∃* 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩

Proof

Step Hyp Ref Expression
1 moop2.1 ⊢ 𝐵 ∈ V
2 eqtr2 ⊢ ( ( 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ∧ 𝐴 = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ ) → ⟨ 𝐵 , 𝑥 ⟩ = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ )
3 vex ⊢ 𝑥 ∈ V
4 1 3 opth ⊢ ( ⟨ 𝐵 , 𝑥 ⟩ = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ ↔ ( 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∧ 𝑥 = 𝑦 ) )
5 4 simprbi ⊢ ( ⟨ 𝐵 , 𝑥 ⟩ = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ → 𝑥 = 𝑦 )
6 2 5 syl ⊢ ( ( 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ∧ 𝐴 = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ ) → 𝑥 = 𝑦 )
7 6 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ( ( 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ∧ 𝐴 = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ ) → 𝑥 = 𝑦 )
8 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
9 nfcv ⊢ Ⅎ 𝑥 𝑦
10 8 9 nfop ⊢ Ⅎ 𝑥 ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩
11 10 nfeq2 ⊢ Ⅎ 𝑥 𝐴 = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩
12 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
13 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
14 12 13 opeq12d ⊢ ( 𝑥 = 𝑦 → ⟨ 𝐵 , 𝑥 ⟩ = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ )
15 14 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ↔ 𝐴 = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ ) )
16 11 15 mo4f ⊢ ( ∃* 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ∧ 𝐴 = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , 𝑦 ⟩ ) → 𝑥 = 𝑦 ) )
17 7 16 mpbir ⊢ ∃* 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩