Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xpexd | Structured version Visualization version GIF version |
Description: The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
xpexd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
xpexd.2 | ⊢ (𝜑 → 𝐵 ∈ 𝑊) |
Ref | Expression |
---|---|
xpexd | ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpexd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | xpexd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
3 | xpexg 7462 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 Vcvv 3492 × cxp 5546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-opab 5120 df-xp 5554 df-rel 5555 |
This theorem is referenced by: cnvexg 7618 cofunexg 7639 oprabexd 7665 ofmresex 7675 opabex2 7744 offval22 7772 tposexg 7895 marypha1 8886 wdom2d 9032 ixpiunwdom 9043 fnct 9947 fpwwe2lem2 10042 fpwwe2lem5 10044 fpwwe2lem12 10051 fpwwelem 10055 canthwe 10061 pwxpndom 10076 gchhar 10089 trclexlem 14342 isacs1i 16916 brcic 17056 rescval2 17086 reschom 17088 rescabs 17091 setccofval 17330 estrccofval 17367 sylow2a 18673 lsmhash 18760 gsumxp 19025 gsumxp2 19029 opsrval 20183 opsrtoslem2 20193 evlslem4 20216 matbas2d 20960 tsmsxp 22690 ustssel 22741 ustfilxp 22748 trust 22765 restutop 22773 trcfilu 22830 cfiluweak 22831 imasdsf1olem 22910 metustfbas 23094 restmetu 23107 rrxsca 23926 perpln1 26423 perpln2 26424 isperp 26425 suppovss 30354 fsuppcurry1 30387 fsuppcurry2 30388 hashxpe 30455 fedgmullem1 30924 fedgmullem2 30925 fedgmul 30926 metidval 31029 esumiun 31252 madeval 33186 filnetlem3 33625 bj-imdirval 34364 bj-imdirval2 34365 isrngod 35057 isgrpda 35114 iscringd 35157 wdom2d2 39510 unxpwdom3 39573 trclubgNEW 39856 relexpxpmin 39940 rfovd 40225 rfovcnvf1od 40228 fsovrfovd 40233 dvsinax 42073 sge0xp 42588 |
Copyright terms: Public domain | W3C validator |