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) Avoid ax-nul . (Revised by GG, 6-Mar-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | opex | |- <. A , B >. e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-op | |- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) } |
|
| 2 | simp3 | |- ( ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) -> x e. { { A } , { A , B } } ) |
|
| 3 | prex | |- { { A } , { A , B } } e. _V |
|
| 4 | 2 3 | abex | |- { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) } e. _V |
| 5 | 1 4 | eqeltri | |- <. A , B >. e. _V |