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 5140 | 1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1483 × cxp 5112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-opab 4713 df-xp 5120 |
This theorem is referenced by: xpcoid 5676 hartogslem1 8447 isfin6 9122 fpwwe2cbv 9452 fpwwe2lem2 9454 fpwwe2lem3 9455 fpwwe2lem8 9459 fpwwe2lem12 9463 fpwwe2lem13 9464 fpwwe2 9465 fpwwecbv 9466 fpwwelem 9467 canthwelem 9472 canthwe 9473 pwfseqlem4 9484 prdsval 16115 imasval 16171 imasaddfnlem 16188 comfffval 16358 comfeq 16366 oppcval 16373 sscfn1 16477 sscfn2 16478 isssc 16480 ssceq 16486 reschomf 16491 isfunc 16524 idfuval 16536 funcres 16556 funcpropd 16560 fucval 16618 fucpropd 16637 homafval 16679 setcval 16727 catcval 16746 estrcval 16764 estrchomfeqhom 16776 hofval 16892 hofpropd 16907 islat 17047 istsr 17217 cnvtsr 17222 isdir 17232 tsrdir 17238 intopsn 17253 frmdval 17388 resgrpplusfrn 17436 opsrval 19474 matval 20217 ustval 22006 trust 22033 utop2nei 22054 utop3cls 22055 utopreg 22056 ussval 22063 ressuss 22067 tususs 22074 fmucnd 22096 cfilufg 22097 trcfilu 22098 neipcfilu 22100 ispsmet 22109 prdsdsf 22172 prdsxmet 22174 ressprdsds 22176 xpsdsfn2 22183 xpsxmetlem 22184 xpsmet 22187 isxms 22252 isms 22254 xmspropd 22278 mspropd 22279 setsxms 22284 setsms 22285 imasf1oxms 22294 imasf1oms 22295 ressxms 22330 ressms 22331 prdsxmslem2 22334 metuval 22354 nmpropd2 22399 ngppropd 22441 tngngp2 22456 pi1addf 22847 pi1addval 22848 iscms 23142 cmspropd 23146 cmsss 23147 rrxds 23181 rrxmfval 23189 minveclem3a 23198 dvlip2 23758 dchrval 24959 brcgr 25780 issh 28065 qtophaus 29903 prsssdm 29963 ordtrestNEW 29967 ordtrest2NEW 29969 isrrext 30044 sibfof 30402 mdvval 31401 msrval 31435 mthmpps 31479 madeval 31935 funtransport 32138 fvtransport 32139 bj-diagval 33090 prdsbnd2 33594 cnpwstotbnd 33596 isrngo 33696 isrngod 33697 rngosn3 33723 isdivrngo 33749 drngoi 33750 isgrpda 33754 ldualset 34412 aomclem8 37631 intopval 41838 rngcvalALTV 41961 rngcval 41962 rnghmsubcsetclem1 41975 rngccat 41978 rngchomrnghmresALTV 41996 ringcvalALTV 42007 ringcval 42008 rhmsubcsetclem1 42021 ringccat 42024 rhmsubcrngclem1 42027 rhmsubcrngc 42029 srhmsubc 42076 rhmsubc 42090 srhmsubcALTV 42094 elpglem3 42456 |
Copyright terms: Public domain | W3C validator |