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 5621 | 1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 × cxp 5588 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-opab 5138 df-xp 5596 |
This theorem is referenced by: xpcoid 6197 hartogslem1 9310 isfin6 10065 fpwwe2cbv 10395 fpwwe2lem2 10397 fpwwe2lem3 10398 fpwwe2lem7 10402 fpwwe2lem11 10406 fpwwe2lem12 10407 fpwwe2 10408 fpwwecbv 10409 fpwwelem 10410 canthwelem 10415 canthwe 10416 pwfseqlem4 10427 prdsval 17175 imasval 17231 imasaddfnlem 17248 comfffval 17416 comfeq 17424 oppcval 17431 sscfn1 17538 sscfn2 17539 isssc 17541 ssceq 17547 reschomf 17553 isfunc 17588 idfuval 17600 funcres 17620 funcpropd 17625 fucval 17684 fucpropd 17704 homafval 17753 setcval 17801 catcval 17824 estrcval 17849 estrchomfeqhom 17861 hofval 17979 hofpropd 17994 islat 18160 istsr 18310 cnvtsr 18315 isdir 18325 tsrdir 18331 intopsn 18347 frmdval 18499 resgrpplusfrn 18602 opsrval 21256 matval 21567 ustval 23363 trust 23390 utop2nei 23411 utop3cls 23412 utopreg 23413 ussval 23420 ressuss 23423 tususs 23431 fmucnd 23453 cfilufg 23454 trcfilu 23455 neipcfilu 23457 ispsmet 23466 prdsdsf 23529 prdsxmet 23531 ressprdsds 23533 xpsdsfn2 23540 xpsxmetlem 23541 xpsmet 23544 isxms 23609 isms 23611 xmspropd 23635 mspropd 23636 setsxms 23643 setsms 23644 imasf1oxms 23654 imasf1oms 23655 ressxms 23690 ressms 23691 prdsxmslem2 23694 metuval 23714 nmpropd2 23760 ngppropd 23802 tngngp2 23825 pi1addf 24219 pi1addval 24220 iscms 24518 cmspropd 24522 cmssmscld 24523 cmsss 24524 cssbn 24548 rrxds 24566 rrxmfval 24579 minveclem3a 24600 dvlip2 25168 dchrval 26391 brcgr 27277 issh 29579 qtophaus 31795 prsssdm 31876 ordtrestNEW 31880 ordtrest2NEW 31882 isrrext 31959 sibfof 32316 satefv 33385 mdvval 33475 msrval 33509 mthmpps 33553 madeval 34045 funtransport 34342 fvtransport 34343 prdsbnd2 35962 cnpwstotbnd 35964 isrngo 36064 isrngod 36065 rngosn3 36091 isdivrngo 36117 drngoi 36118 isgrpda 36122 ldualset 37146 aomclem8 40893 intopval 45407 rngcvalALTV 45530 rngcval 45531 rnghmsubcsetclem1 45544 rngccat 45547 rngchomrnghmresALTV 45565 ringcvalALTV 45576 ringcval 45577 rhmsubcsetclem1 45590 ringccat 45593 rhmsubcrngclem1 45596 rhmsubcrngc 45598 srhmsubc 45645 rhmsubc 45659 srhmsubcALTV 45663 elpglem3 46429 |
Copyright terms: Public domain | W3C validator |