Description: A pair of two sets belongs to the power class of a class containing those two sets and vice versa. (Contributed by AV, 8-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | prelpw | |- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } e. ~P C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prssg | |- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) ) |
|
2 | prex | |- { A , B } e. _V |
|
3 | 2 | elpw | |- ( { A , B } e. ~P C <-> { A , B } C_ C ) |
4 | 1 3 | bitr4di | |- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } e. ~P C ) ) |