Metamath Proof Explorer

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 e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )

Proof

Step Hyp Ref Expression
1 elxp2 
 |-  ( A e. ( _V X. _V ) <-> E. x e. _V E. y e. _V A = <. x , y >. )
2 rexv 
 |-  ( E. x e. _V E. y e. _V A = <. x , y >. <-> E. x E. y e. _V A = <. x , y >. )
3 rexv 
 |-  ( E. y e. _V A = <. x , y >. <-> E. y A = <. x , y >. )
4 3 exbii 
 |-  ( E. x E. y e. _V A = <. x , y >. <-> E. x E. y A = <. x , y >. )
5 1 2 4 3bitri 
 |-  ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )