# Metamath Proof Explorer

## Theorem elvv

Description: Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994)

Ref Expression
Assertion elvv ${⊢}{A}\in \left(\mathrm{V}×\mathrm{V}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{A}=⟨{x},{y}⟩$

### Proof

Step Hyp Ref Expression
1 elxp ${⊢}{A}\in \left(\mathrm{V}×\mathrm{V}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in \mathrm{V}\wedge {y}\in \mathrm{V}\right)\right)$
2 vex ${⊢}{x}\in \mathrm{V}$
3 vex ${⊢}{y}\in \mathrm{V}$
4 2 3 pm3.2i ${⊢}\left({x}\in \mathrm{V}\wedge {y}\in \mathrm{V}\right)$
5 4 biantru ${⊢}{A}=⟨{x},{y}⟩↔\left({A}=⟨{x},{y}⟩\wedge \left({x}\in \mathrm{V}\wedge {y}\in \mathrm{V}\right)\right)$
6 5 2exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{A}=⟨{x},{y}⟩↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in \mathrm{V}\wedge {y}\in \mathrm{V}\right)\right)$
7 1 6 bitr4i ${⊢}{A}\in \left(\mathrm{V}×\mathrm{V}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{A}=⟨{x},{y}⟩$