Theorem elvv

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

	Ref	Expression
Assertion	elvv	|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )

Proof

Step	Hyp	Ref	Expression
1		elxp	|- ( A e. ( _V X. _V ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
2		vex	|- x e. _V
3		vex	|- y e. _V
4	2 3	pm3.2i	|- ( x e. _V /\ y e. _V )
5	4	biantru	|- ( A = <. x , y >. <-> ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
6	5	2exbii	|- ( E. x E. y A = <. x , y >. <-> E. x E. y ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
7	1 6	bitr4i	|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )