Description: An ordered pair is nonempty iff the arguments are sets. (Contributed by NM, 24-Jan-2004) (Revised by Mario Carneiro, 26-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | opnz | |- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opprc | |- ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) ) |
|
2 | 1 | necon1ai | |- ( <. A , B >. =/= (/) -> ( A e. _V /\ B e. _V ) ) |
3 | dfopg | |- ( ( A e. _V /\ B e. _V ) -> <. A , B >. = { { A } , { A , B } } ) |
|
4 | snex | |- { A } e. _V |
|
5 | 4 | prnz | |- { { A } , { A , B } } =/= (/) |
6 | 5 | a1i | |- ( ( A e. _V /\ B e. _V ) -> { { A } , { A , B } } =/= (/) ) |
7 | 3 6 | eqnetrd | |- ( ( A e. _V /\ B e. _V ) -> <. A , B >. =/= (/) ) |
8 | 2 7 | impbii | |- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) ) |