Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of Monk1 p. 37. (Contributed by NM, 12-Apr-2004) Avoid axioms. (Revised by TM, 1-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xp0 | |- ( A X. (/) ) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | noel | |- -. y e. (/) |
|
| 2 | simprr | |- ( ( z = <. x , y >. /\ ( x e. A /\ y e. (/) ) ) -> y e. (/) ) |
|
| 3 | 1 2 | mto | |- -. ( z = <. x , y >. /\ ( x e. A /\ y e. (/) ) ) |
| 4 | 3 | nex | |- -. E. y ( z = <. x , y >. /\ ( x e. A /\ y e. (/) ) ) |
| 5 | 4 | nex | |- -. E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. (/) ) ) |
| 6 | elxpi | |- ( z e. ( A X. (/) ) -> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. (/) ) ) ) |
|
| 7 | 5 6 | mto | |- -. z e. ( A X. (/) ) |
| 8 | 7 | nel0 | |- ( A X. (/) ) = (/) |