| 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 5716 | 1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 × cxp 5683 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-opab 5206 df-xp 5691 |
| This theorem is referenced by: xpcoid 6310 hartogslem1 9582 isfin6 10340 fpwwe2cbv 10670 fpwwe2lem2 10672 fpwwe2lem3 10673 fpwwe2lem4 10674 fpwwe2lem7 10677 fpwwe2lem11 10681 fpwwe2lem12 10682 fpwwe2 10683 fpwwecbv 10684 fpwwelem 10685 canthwelem 10690 canthwe 10691 pwfseqlem4 10702 prdsval 17500 imasval 17556 imasaddfnlem 17573 comfffval 17741 comfeq 17749 oppcval 17756 sscfn1 17861 sscfn2 17862 isssc 17864 ssceq 17870 reschomf 17875 isfunc 17909 idfuval 17921 funcres 17941 funcpropd 17947 fucval 18006 fucpropd 18025 homafval 18074 setcval 18122 catcval 18145 estrcval 18168 estrchomfeqhom 18180 hofval 18297 hofpropd 18312 islat 18478 istsr 18628 cnvtsr 18633 isdir 18643 tsrdir 18649 intopsn 18667 frmdval 18864 resgrpplusfrn 18968 rngcval 20618 rnghmsubcsetclem1 20631 rngccat 20634 ringcval 20647 rhmsubcsetclem1 20660 ringccat 20663 rhmsubcrngclem1 20666 rhmsubcrngc 20668 srhmsubc 20680 rhmsubc 20689 opsrval 22064 matval 22415 ustval 24211 trust 24238 utop2nei 24259 utop3cls 24260 utopreg 24261 ussval 24268 ressuss 24271 tususs 24279 fmucnd 24301 cfilufg 24302 trcfilu 24303 neipcfilu 24305 ispsmet 24314 prdsdsf 24377 prdsxmet 24379 ressprdsds 24381 xpsdsfn2 24388 xpsxmetlem 24389 xpsmet 24392 isxms 24457 isms 24459 xmspropd 24483 mspropd 24484 setsxms 24491 setsms 24492 imasf1oxms 24502 imasf1oms 24503 ressxms 24538 ressms 24539 prdsxmslem2 24542 metuval 24562 nmpropd2 24608 ngppropd 24650 tngngp2 24673 pi1addf 25080 pi1addval 25081 iscms 25379 cmspropd 25383 cmssmscld 25384 cmsss 25385 cssbn 25409 rrxds 25427 rrxmfval 25440 minveclem3a 25461 dvlip2 26034 dchrval 27278 madeval 27891 brcgr 28915 issh 31227 qtophaus 33835 prsssdm 33916 ordtrestNEW 33920 ordtrest2NEW 33922 isrrext 34001 sibfof 34342 satefv 35419 mdvval 35509 msrval 35543 mthmpps 35587 funtransport 36032 fvtransport 36033 prdsbnd2 37802 cnpwstotbnd 37804 isrngo 37904 isrngod 37905 rngosn3 37931 isdivrngo 37957 drngoi 37958 isgrpda 37962 ldualset 39126 aomclem8 43073 intopval 48118 rngcvalALTV 48181 rngchomrnghmresALTV 48195 ringcvalALTV 48205 srhmsubcALTV 48241 0funcg2 48917 elpglem3 49232 pgindnf 49235 |
| Copyright terms: Public domain | W3C validator |