| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > xpex | Structured version Visualization version GIF version | ||
| Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.) |
| Ref | Expression |
|---|---|
| xpex.1 | ⊢ 𝐴 ∈ V |
| xpex.2 | ⊢ 𝐵 ∈ V |
| Ref | Expression |
|---|---|
| xpex | ⊢ (𝐴 × 𝐵) ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpex.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | xpex.2 | . 2 ⊢ 𝐵 ∈ V | |
| 3 | xpexg 7770 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 × 𝐵) ∈ V |
| Copyright terms: Public domain | W3C validator |