![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpsng | Structured version Visualization version GIF version |
Description: The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.) |
Ref | Expression |
---|---|
xpsng | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg 6392 | . . 3 ⊢ (𝐵 ∈ 𝑊 → ({𝐴} × {𝐵}):{𝐴}⟶{𝐵}) | |
2 | 1 | adantl 474 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}):{𝐴}⟶{𝐵}) |
3 | fsng 6720 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (({𝐴} × {𝐵}):{𝐴}⟶{𝐵} ↔ ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉})) | |
4 | 2, 3 | mpbid 224 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 {csn 4435 〈cop 4441 × cxp 5401 ⟶wf 6181 |
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-13 2301 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pr 5182 |
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-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 |
This theorem is referenced by: xpprsng 6723 xpsn 6724 f1o2sn 6725 residpr 6726 fmptsn 6750 mposn 7604 repsw1 14000 s1co 14055 xpscg 16685 xpsc0 16689 xpsc1 16690 intopsn 17733 grp1inv 18006 psgnsn 18422 ixpsnbasval 19715 mat1dimelbas 20796 mat1dimscm 20800 mat1dimmul 20801 mat1f1o 20803 m1detdiag 20922 pt1hmeo 22130 cosnop 30204 cshw1s2 30390 nosupbnd2lem1 32765 rngosn3 34673 fmptsnxp 40875 lmod1zr 43940 |
Copyright terms: Public domain | W3C validator |