| 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 7770 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | |
| 4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3480 × cxp 5683 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-opab 5206 df-xp 5691 df-rel 5692 |
| This theorem is referenced by: cnvexg 7946 fabexd 7959 cofunexg 7973 oprabexd 8000 ofmresex 8010 opabex2 8082 offval22 8113 sexp2 8171 sexp3 8178 tposexg 8265 mapunen 9186 marypha1 9474 wdom2d 9620 ixpiunwdom 9630 ttrclexg 9763 fnct 10577 fpwwe2lem2 10672 fpwwe2lem4 10674 fpwwe2lem11 10681 fpwwelem 10685 canthwe 10691 pwxpndom 10706 gchhar 10719 trclexlem 15033 isacs1i 17700 brcic 17842 rescval2 17872 reschom 17874 rescabs 17877 rescabsOLD 17878 setccofval 18127 estrccofval 18173 sylow2a 19637 gsumxp 19994 gsumxp2 19998 opsrval 22064 opsrtoslem2 22080 evlslem4 22100 matbas2d 22429 tsmsxp 24163 ustssel 24214 ustfilxp 24221 trust 24238 restutop 24246 trcfilu 24303 cfiluweak 24304 imasdsf1olem 24383 metustfbas 24570 restmetu 24583 rrxsca 25430 madeval 27891 perpln1 28718 perpln2 28719 isperp 28720 suppovss 32690 fsuppcurry1 32736 fsuppcurry2 32737 hashxpe 32811 gsumpart 33060 gsumwrd2dccat 33070 elrgspnlem2 33247 elrgspnsubrunlem2 33252 erlval 33262 rlocval 33263 rlocbas 33271 rlocaddval 33272 rlocmulval 33273 fedgmullem1 33680 fedgmullem2 33681 fedgmul 33682 metidval 33889 esumiun 34095 filnetlem3 36381 numiunnum 36471 bj-imdirvallem 37181 bj-imdirval2 37184 bj-imdirco 37191 bj-iminvval2 37195 isrngod 37905 isgrpda 37962 iscringd 38005 aks6d1c6lem2 42172 evlsevl 42581 wdom2d2 43047 unxpwdom3 43107 trclubgNEW 43631 relexpxpmin 43730 rfovd 44014 rfovcnvf1od 44017 fsovrfovd 44022 dvsinax 45928 sge0xp 46444 gpgvtx 48002 gpgiedg 48003 fucofvalg 49013 |
| Copyright terms: Public domain | W3C validator |