Theorem elvv

Description: Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994) (Proof shortened by BJ, 16-Oct-2026)

	Ref	Expression
Assertion	elvv	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yA=⟨x,y⟩$$

Proof

Step	Hyp	Ref	Expression
1		elxp2	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\in \mathrm{V}\exists y\in \mathrm{V}A=⟨x,y⟩$$
2		rexv	$$⊢\exists x\in \mathrm{V}\exists y\in \mathrm{V}A=⟨x,y⟩\leftrightarrow \exists x\exists y\in \mathrm{V}A=⟨x,y⟩$$
3		rexv	$$⊢\exists y\in \mathrm{V}A=⟨x,y⟩\leftrightarrow \exists yA=⟨x,y⟩$$
4	3	exbii	$$⊢\exists x\exists y\in \mathrm{V}A=⟨x,y⟩\leftrightarrow \exists x\exists yA=⟨x,y⟩$$
5	1 2 4	3bitri	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yA=⟨x,y⟩$$