Description: An ordered pair of classes is a set. Exercise 7 of TakeutiZaring p. 16. (Contributed by NM, 18-Aug-1993) (Revised by Mario Carneiro, 26-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | opex | |- <. A , B >. e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfopif | |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) |
|
| 2 | prex | |- { { A } , { A , B } } e. _V |
|
| 3 | 0ex | |- (/) e. _V |
|
| 4 | 2 3 | ifex | |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V |
| 5 | 1 4 | eqeltri | |- <. A , B >. e. _V |