![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sqxpeqd | Structured version Visualization version GIF version |
Description: Equality deduction for a Cartesian square, see Wikipedia "Cartesian product", https://en.wikipedia.org/wiki/Cartesian_product#n-ary_Cartesian_power. (Contributed by AV, 13-Jan-2020.) |
Ref | Expression |
---|---|
xpeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
sqxpeqd | ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1, 1 | xpeq12d 5709 | 1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 × cxp 5676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-opab 5211 df-xp 5684 |
This theorem is referenced by: xpcoid 6294 hartogslem1 9565 isfin6 10323 fpwwe2cbv 10653 fpwwe2lem2 10655 fpwwe2lem3 10656 fpwwe2lem7 10660 fpwwe2lem11 10664 fpwwe2lem12 10665 fpwwe2 10666 fpwwecbv 10667 fpwwelem 10668 canthwelem 10673 canthwe 10674 pwfseqlem4 10685 prdsval 17436 imasval 17492 imasaddfnlem 17509 comfffval 17677 comfeq 17685 oppcval 17692 sscfn1 17799 sscfn2 17800 isssc 17802 ssceq 17808 reschomf 17814 isfunc 17849 idfuval 17861 funcres 17881 funcpropd 17888 fucval 17948 fucpropd 17968 homafval 18017 setcval 18065 catcval 18088 estrcval 18113 estrchomfeqhom 18125 hofval 18243 hofpropd 18258 islat 18424 istsr 18574 cnvtsr 18579 isdir 18589 tsrdir 18595 intopsn 18613 frmdval 18802 resgrpplusfrn 18906 rngcval 20550 rnghmsubcsetclem1 20563 rngccat 20566 ringcval 20579 rhmsubcsetclem1 20592 ringccat 20595 rhmsubcrngclem1 20598 rhmsubcrngc 20600 srhmsubc 20612 rhmsubc 20621 opsrval 21983 matval 22310 ustval 24106 trust 24133 utop2nei 24154 utop3cls 24155 utopreg 24156 ussval 24163 ressuss 24166 tususs 24174 fmucnd 24196 cfilufg 24197 trcfilu 24198 neipcfilu 24200 ispsmet 24209 prdsdsf 24272 prdsxmet 24274 ressprdsds 24276 xpsdsfn2 24283 xpsxmetlem 24284 xpsmet 24287 isxms 24352 isms 24354 xmspropd 24378 mspropd 24379 setsxms 24386 setsms 24387 imasf1oxms 24397 imasf1oms 24398 ressxms 24433 ressms 24434 prdsxmslem2 24437 metuval 24457 nmpropd2 24503 ngppropd 24545 tngngp2 24568 pi1addf 24973 pi1addval 24974 iscms 25272 cmspropd 25276 cmssmscld 25277 cmsss 25278 cssbn 25302 rrxds 25320 rrxmfval 25333 minveclem3a 25354 dvlip2 25927 dchrval 27166 madeval 27778 brcgr 28710 issh 31017 qtophaus 33437 prsssdm 33518 ordtrestNEW 33522 ordtrest2NEW 33524 isrrext 33601 sibfof 33960 satefv 35024 mdvval 35114 msrval 35148 mthmpps 35192 funtransport 35627 fvtransport 35628 prdsbnd2 37268 cnpwstotbnd 37270 isrngo 37370 isrngod 37371 rngosn3 37397 isdivrngo 37423 drngoi 37424 isgrpda 37428 ldualset 38597 aomclem8 42485 intopval 47264 rngcvalALTV 47327 rngchomrnghmresALTV 47341 ringcvalALTV 47351 srhmsubcALTV 47387 elpglem3 48144 pgindnf 48147 |
Copyright terms: Public domain | W3C validator |