Description: Ordered pair membership in the universal class of ordered pairs. (Contributed by NM, 22-Aug-2013) (Revised by Mario Carneiro, 26-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | opelvv.1 | |- A e. _V |
|
| opelvv.2 | |- B e. _V |
||
| Assertion | opelvv | |- <. A , B >. e. ( _V X. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opelvv.1 | |- A e. _V |
|
| 2 | opelvv.2 | |- B e. _V |
|
| 3 | opelxpi | |- ( ( A e. _V /\ B e. _V ) -> <. A , B >. e. ( _V X. _V ) ) |
|
| 4 | 1 2 3 | mp2an | |- <. A , B >. e. ( _V X. _V ) |