Metamath Proof Explorer

Theorem altopex

Description: Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012)

Ref Expression
Assertion altopex 
|- << A , B >> e. _V

Proof

Step Hyp Ref Expression
1 df-altop 
 |-  << A , B >> = { { A } , { A , { B } } }
2 prex 
 |-  { { A } , { A , { B } } } e. _V
3 1 2 eqeltri 
 |-  << A , B >> e. _V