theorem prelxp (A B: set) (a b: nat): $ a, b e. Xp A B <-> a e. A /\ b e. B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsidd | x = a -> B == B |
|
2 | 1 | elxab | a, b e. X\ x e. A, B <-> a e. A /\ b e. B |
3 | 2 | conv Xp | a, b e. Xp A B <-> a e. A /\ b e. B |