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

Metamath Proof Explorer

Theorem eqvinop

Description: A variable introduction law for ordered pairs. Analogue of Lemma 15 of Monk2 p. 109. (Contributed by NM, 28-May-1995)

Ref Expression
Hypotheses eqvinop.1 ⊢ 𝐵 ∈ V
eqvinop.2 ⊢ 𝐶 ∈ V
Assertion eqvinop ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )

Proof

Step Hyp Ref Expression
1 eqvinop.1 ⊢ 𝐵 ∈ V
2 eqvinop.2 ⊢ 𝐶 ∈ V
3 1 2 opth2 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) )
4 3 anbi2i ⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ) )
5 ancom ⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ) ↔ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6 anass ⊢ ( ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
7 4 5 6 3bitri ⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
8 7 exbii ⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑦 ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
9 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( 𝑥 = 𝐵 ∧ ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
10 opeq2 ⊢ ( 𝑦 = 𝐶 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝐶 ⟩ )
11 10 eqeq2d ⊢ ( 𝑦 = 𝐶 → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) )
12 2 11 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ )
13 12 anbi2i ⊢ ( ( 𝑥 = 𝐵 ∧ ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) )
14 8 9 13 3bitri ⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) )
15 14 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) )
16 opeq1 ⊢ ( 𝑥 = 𝐵 → ⟨ 𝑥 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
17 16 eqeq2d ⊢ ( 𝑥 = 𝐵 → ( 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ↔ 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ) )
18 1 17 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) ↔ 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ )
19 15 18 bitr2i ⊢ ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )