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 ⊢ B ∈ V
eqvinop.2 ⊢ C ∈ V
Assertion eqvinop ⊢ A = B C ↔ ∃ x ∃ y A = x y ∧ x y = B C

Proof

Step Hyp Ref Expression
1 eqvinop.1 ⊢ B ∈ V
2 eqvinop.2 ⊢ C ∈ V
3 1 2 opth2 ⊢ x y = B C ↔ x = B ∧ y = C
4 3 anbi2i ⊢ A = x y ∧ x y = B C ↔ A = x y ∧ x = B ∧ y = C
5 ancom ⊢ A = x y ∧ x = B ∧ y = C ↔ x = B ∧ y = C ∧ A = x y
6 anass ⊢ x = B ∧ y = C ∧ A = x y ↔ x = B ∧ y = C ∧ A = x y
7 4 5 6 3bitri ⊢ A = x y ∧ x y = B C ↔ x = B ∧ y = C ∧ A = x y
8 7 exbii ⊢ ∃ y A = x y ∧ x y = B C ↔ ∃ y x = B ∧ y = C ∧ A = x y
9 19.42v ⊢ ∃ y x = B ∧ y = C ∧ A = x y ↔ x = B ∧ ∃ y y = C ∧ A = x y
10 opeq2 ⊢ y = C → x y = x C
11 10 eqeq2d ⊢ y = C → A = x y ↔ A = x C
12 2 11 ceqsexv ⊢ ∃ y y = C ∧ A = x y ↔ A = x C
13 12 anbi2i ⊢ x = B ∧ ∃ y y = C ∧ A = x y ↔ x = B ∧ A = x C
14 8 9 13 3bitri ⊢ ∃ y A = x y ∧ x y = B C ↔ x = B ∧ A = x C
15 14 exbii ⊢ ∃ x ∃ y A = x y ∧ x y = B C ↔ ∃ x x = B ∧ A = x C
16 opeq1 ⊢ x = B → x C = B C
17 16 eqeq2d ⊢ x = B → A = x C ↔ A = B C
18 1 17 ceqsexv ⊢ ∃ x x = B ∧ A = x C ↔ A = B C
19 15 18 bitr2i ⊢ A = B C ↔ ∃ x ∃ y A = x y ∧ x y = B C