# 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}\in \mathrm{V}$
eqvinop.2 ${⊢}{C}\in \mathrm{V}$
Assertion eqvinop ${⊢}{A}=⟨{B},{C}⟩↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge ⟨{x},{y}⟩=⟨{B},{C}⟩\right)$

### Proof

Step Hyp Ref Expression
1 eqvinop.1 ${⊢}{B}\in \mathrm{V}$
2 eqvinop.2 ${⊢}{C}\in \mathrm{V}$
3 1 2 opth2 ${⊢}⟨{x},{y}⟩=⟨{B},{C}⟩↔\left({x}={B}\wedge {y}={C}\right)$
4 3 anbi2i ${⊢}\left({A}=⟨{x},{y}⟩\wedge ⟨{x},{y}⟩=⟨{B},{C}⟩\right)↔\left({A}=⟨{x},{y}⟩\wedge \left({x}={B}\wedge {y}={C}\right)\right)$
5 ancom ${⊢}\left({A}=⟨{x},{y}⟩\wedge \left({x}={B}\wedge {y}={C}\right)\right)↔\left(\left({x}={B}\wedge {y}={C}\right)\wedge {A}=⟨{x},{y}⟩\right)$
6 anass ${⊢}\left(\left({x}={B}\wedge {y}={C}\right)\wedge {A}=⟨{x},{y}⟩\right)↔\left({x}={B}\wedge \left({y}={C}\wedge {A}=⟨{x},{y}⟩\right)\right)$
7 4 5 6 3bitri ${⊢}\left({A}=⟨{x},{y}⟩\wedge ⟨{x},{y}⟩=⟨{B},{C}⟩\right)↔\left({x}={B}\wedge \left({y}={C}\wedge {A}=⟨{x},{y}⟩\right)\right)$
8 7 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge ⟨{x},{y}⟩=⟨{B},{C}⟩\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={B}\wedge \left({y}={C}\wedge {A}=⟨{x},{y}⟩\right)\right)$
9 19.42v ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={B}\wedge \left({y}={C}\wedge {A}=⟨{x},{y}⟩\right)\right)↔\left({x}={B}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={C}\wedge {A}=⟨{x},{y}⟩\right)\right)$
10 opeq2 ${⊢}{y}={C}\to ⟨{x},{y}⟩=⟨{x},{C}⟩$
11 10 eqeq2d ${⊢}{y}={C}\to \left({A}=⟨{x},{y}⟩↔{A}=⟨{x},{C}⟩\right)$
12 2 11 ceqsexv ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={C}\wedge {A}=⟨{x},{y}⟩\right)↔{A}=⟨{x},{C}⟩$
13 12 anbi2i ${⊢}\left({x}={B}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={C}\wedge {A}=⟨{x},{y}⟩\right)\right)↔\left({x}={B}\wedge {A}=⟨{x},{C}⟩\right)$
14 8 9 13 3bitri ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge ⟨{x},{y}⟩=⟨{B},{C}⟩\right)↔\left({x}={B}\wedge {A}=⟨{x},{C}⟩\right)$
15 14 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge ⟨{x},{y}⟩=⟨{B},{C}⟩\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={B}\wedge {A}=⟨{x},{C}⟩\right)$
16 opeq1 ${⊢}{x}={B}\to ⟨{x},{C}⟩=⟨{B},{C}⟩$
17 16 eqeq2d ${⊢}{x}={B}\to \left({A}=⟨{x},{C}⟩↔{A}=⟨{B},{C}⟩\right)$
18 1 17 ceqsexv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={B}\wedge {A}=⟨{x},{C}⟩\right)↔{A}=⟨{B},{C}⟩$
19 15 18 bitr2i ${⊢}{A}=⟨{B},{C}⟩↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge ⟨{x},{y}⟩=⟨{B},{C}⟩\right)$