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 ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )