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 5556 | 1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 × cxp 5523 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-opab 5093 df-xp 5531 |
This theorem is referenced by: xpcoid 6122 hartogslem1 9079 isfin6 9800 fpwwe2cbv 10130 fpwwe2lem2 10132 fpwwe2lem3 10133 fpwwe2lem7 10137 fpwwe2lem11 10141 fpwwe2lem12 10142 fpwwe2 10143 fpwwecbv 10144 fpwwelem 10145 canthwelem 10150 canthwe 10151 pwfseqlem4 10162 prdsval 16831 imasval 16887 imasaddfnlem 16904 comfffval 17072 comfeq 17080 oppcval 17087 sscfn1 17192 sscfn2 17193 isssc 17195 ssceq 17201 reschomf 17206 isfunc 17239 idfuval 17251 funcres 17271 funcpropd 17275 fucval 17333 fucpropd 17352 homafval 17401 setcval 17449 catcval 17472 estrcval 17490 estrchomfeqhom 17502 hofval 17618 hofpropd 17633 islat 17773 istsr 17943 cnvtsr 17948 isdir 17958 tsrdir 17964 intopsn 17980 frmdval 18132 resgrpplusfrn 18235 opsrval 20857 matval 21162 ustval 22954 trust 22981 utop2nei 23002 utop3cls 23003 utopreg 23004 ussval 23011 ressuss 23015 tususs 23022 fmucnd 23044 cfilufg 23045 trcfilu 23046 neipcfilu 23048 ispsmet 23057 prdsdsf 23120 prdsxmet 23122 ressprdsds 23124 xpsdsfn2 23131 xpsxmetlem 23132 xpsmet 23135 isxms 23200 isms 23202 xmspropd 23226 mspropd 23227 setsxms 23232 setsms 23233 imasf1oxms 23242 imasf1oms 23243 ressxms 23278 ressms 23279 prdsxmslem2 23282 metuval 23302 nmpropd2 23348 ngppropd 23390 tngngp2 23405 pi1addf 23799 pi1addval 23800 iscms 24097 cmspropd 24101 cmssmscld 24102 cmsss 24103 cssbn 24127 rrxds 24145 rrxmfval 24158 minveclem3a 24179 dvlip2 24747 dchrval 25970 brcgr 26846 issh 29143 qtophaus 31358 prsssdm 31439 ordtrestNEW 31443 ordtrest2NEW 31445 isrrext 31520 sibfof 31877 satefv 32947 mdvval 33037 msrval 33071 mthmpps 33115 madeval 33677 funtransport 33971 fvtransport 33972 prdsbnd2 35576 cnpwstotbnd 35578 isrngo 35678 isrngod 35679 rngosn3 35705 isdivrngo 35731 drngoi 35732 isgrpda 35736 ldualset 36762 aomclem8 40458 intopval 44930 rngcvalALTV 45053 rngcval 45054 rnghmsubcsetclem1 45067 rngccat 45070 rngchomrnghmresALTV 45088 ringcvalALTV 45099 ringcval 45100 rhmsubcsetclem1 45113 ringccat 45116 rhmsubcrngclem1 45119 rhmsubcrngc 45121 srhmsubc 45168 rhmsubc 45182 srhmsubcALTV 45186 elpglem3 45871 |
Copyright terms: Public domain | W3C validator |