![]() |
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 5373 | 1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1656 × cxp 5340 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-opab 4936 df-xp 5348 |
This theorem is referenced by: xpcoid 5917 hartogslem1 8716 isfin6 9437 fpwwe2cbv 9767 fpwwe2lem2 9769 fpwwe2lem3 9770 fpwwe2lem8 9774 fpwwe2lem12 9778 fpwwe2lem13 9779 fpwwe2 9780 fpwwecbv 9781 fpwwelem 9782 canthwelem 9787 canthwe 9788 pwfseqlem4 9799 prdsval 16468 imasval 16524 imasaddfnlem 16541 comfffval 16710 comfeq 16718 oppcval 16725 sscfn1 16829 sscfn2 16830 isssc 16832 ssceq 16838 reschomf 16843 isfunc 16876 idfuval 16888 funcres 16908 funcpropd 16912 fucval 16970 fucpropd 16989 homafval 17031 setcval 17079 catcval 17098 estrcval 17116 estrchomfeqhom 17128 hofval 17245 hofpropd 17260 islat 17400 istsr 17570 cnvtsr 17575 isdir 17585 tsrdir 17591 intopsn 17606 frmdval 17742 resgrpplusfrn 17790 opsrval 19835 matval 20584 ustval 22376 trust 22403 utop2nei 22424 utop3cls 22425 utopreg 22426 ussval 22433 ressuss 22437 tususs 22444 fmucnd 22466 cfilufg 22467 trcfilu 22468 neipcfilu 22470 ispsmet 22479 prdsdsf 22542 prdsxmet 22544 ressprdsds 22546 xpsdsfn2 22553 xpsxmetlem 22554 xpsmet 22557 isxms 22622 isms 22624 xmspropd 22648 mspropd 22649 setsxms 22654 setsms 22655 imasf1oxms 22664 imasf1oms 22665 ressxms 22700 ressms 22701 prdsxmslem2 22704 metuval 22724 nmpropd2 22769 ngppropd 22811 tngngp2 22826 pi1addf 23216 pi1addval 23217 iscms 23513 cmspropd 23517 cmssmscld 23518 cmsss 23519 cssbn 23543 rrxds 23561 rrxmfval 23574 minveclem3a 23595 dvlip2 24157 dchrval 25372 brcgr 26199 issh 28609 qtophaus 30437 prsssdm 30497 ordtrestNEW 30501 ordtrest2NEW 30503 isrrext 30578 sibfof 30936 mdvval 31936 msrval 31970 mthmpps 32014 madeval 32463 funtransport 32666 fvtransport 32667 bj-diagval 33612 prdsbnd2 34129 cnpwstotbnd 34131 isrngo 34231 isrngod 34232 rngosn3 34258 isdivrngo 34284 drngoi 34285 isgrpda 34289 ldualset 35193 aomclem8 38467 intopval 42678 rngcvalALTV 42801 rngcval 42802 rnghmsubcsetclem1 42815 rngccat 42818 rngchomrnghmresALTV 42836 ringcvalALTV 42847 ringcval 42848 rhmsubcsetclem1 42861 ringccat 42864 rhmsubcrngclem1 42867 rhmsubcrngc 42869 srhmsubc 42916 rhmsubc 42930 srhmsubcALTV 42934 elpglem3 43347 |
Copyright terms: Public domain | W3C validator |