![]() |
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 7290 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | |
4 | 1, 2, 3 | syl2anc 576 | 1 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2050 Vcvv 3415 × cxp 5405 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-opab 4992 df-xp 5413 df-rel 5414 |
This theorem is referenced by: cnvexg 7444 cofunexg 7462 oprabexd 7488 ofmresex 7498 opabex2 7563 offval22 7591 tposexg 7709 marypha1 8693 wdom2d 8839 ixpiunwdom 8850 fnct 9757 fpwwe2lem2 9852 fpwwe2lem5 9854 fpwwe2lem12 9861 fpwwelem 9865 canthwe 9871 pwxpndom 9886 gchhar 9899 trclexlem 14215 isacs1i 16786 brcic 16926 rescval2 16956 reschom 16958 rescabs 16961 setccofval 17200 estrccofval 17237 sylow2a 18505 lsmhash 18589 gsumxp 18849 opsrval 19968 opsrtoslem2 19978 evlslem4 20001 matbas2d 20736 tsmsxp 22466 ustssel 22517 ustfilxp 22524 trust 22541 restutop 22549 trcfilu 22606 cfiluweak 22607 imasdsf1olem 22686 metustfbas 22870 restmetu 22883 rrxsca 23702 perpln1 26198 perpln2 26199 isperp 26200 suppovss 30187 fsuppcurry1 30220 fsuppcurry2 30221 hashxpe 30283 fedgmullem1 30660 fedgmullem2 30661 fedgmul 30662 metidval 30780 esumiun 31003 madeval 32816 filnetlem3 33255 isrngod 34624 isgrpda 34681 iscringd 34724 wdom2d2 39034 unxpwdom3 39097 trclubgNEW 39347 relexpxpmin 39431 rfovd 39716 rfovcnvf1od 39719 fsovrfovd 39724 dvsinax 41633 sge0xp 42148 |
Copyright terms: Public domain | W3C validator |