![]() |
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 7757 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | |
4 | 1, 2, 3 | syl2anc 582 | 1 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 Vcvv 3461 × cxp 5679 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5303 ax-nul 5310 ax-pow 5368 ax-pr 5432 ax-un 7745 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4325 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-opab 5215 df-xp 5687 df-rel 5688 |
This theorem is referenced by: cnvexg 7936 fabexd 7947 cofunexg 7961 oprabexd 7988 ofmresex 7998 opabex2 8070 offval22 8101 sexp2 8159 sexp3 8166 tposexg 8254 mapunen 9183 marypha1 9473 wdom2d 9619 ixpiunwdom 9629 ttrclexg 9762 fnct 10576 fpwwe2lem2 10671 fpwwe2lem4 10673 fpwwe2lem11 10680 fpwwelem 10684 canthwe 10690 pwxpndom 10705 gchhar 10718 trclexlem 14994 isacs1i 17665 brcic 17809 rescval2 17839 reschom 17842 rescabs 17846 rescabsOLD 17847 setccofval 18099 estrccofval 18147 sylow2a 19612 gsumxp 19969 gsumxp2 19973 opsrval 22045 opsrtoslem2 22061 evlslem4 22081 matbas2d 22408 tsmsxp 24142 ustssel 24193 ustfilxp 24200 trust 24217 restutop 24225 trcfilu 24282 cfiluweak 24283 imasdsf1olem 24362 metustfbas 24549 restmetu 24562 rrxsca 25407 madeval 27868 perpln1 28629 perpln2 28630 isperp 28631 suppovss 32588 fsuppcurry1 32630 fsuppcurry2 32631 hashxpe 32700 gsumpart 32901 erlval 33090 rlocval 33091 rlocbas 33099 rlocaddval 33100 rlocmulval 33101 fedgmullem1 33496 fedgmullem2 33497 fedgmul 33498 metidval 33661 esumiun 33883 filnetlem3 36040 bj-imdirvallem 36835 bj-imdirval2 36838 bj-imdirco 36845 bj-iminvval2 36849 isrngod 37547 isgrpda 37604 iscringd 37647 aks6d1c6lem2 41817 evlsevl 41985 wdom2d2 42630 unxpwdom3 42693 trclubgNEW 43222 relexpxpmin 43321 rfovd 43605 rfovcnvf1od 43608 fsovrfovd 43613 dvsinax 45471 sge0xp 45987 |
Copyright terms: Public domain | W3C validator |