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 5581 | 1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 × cxp 5548 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-opab 5122 df-xp 5556 |
This theorem is referenced by: xpcoid 6136 hartogslem1 9000 isfin6 9716 fpwwe2cbv 10046 fpwwe2lem2 10048 fpwwe2lem3 10049 fpwwe2lem8 10053 fpwwe2lem12 10057 fpwwe2lem13 10058 fpwwe2 10059 fpwwecbv 10060 fpwwelem 10061 canthwelem 10066 canthwe 10067 pwfseqlem4 10078 prdsval 16722 imasval 16778 imasaddfnlem 16795 comfffval 16962 comfeq 16970 oppcval 16977 sscfn1 17081 sscfn2 17082 isssc 17084 ssceq 17090 reschomf 17095 isfunc 17128 idfuval 17140 funcres 17160 funcpropd 17164 fucval 17222 fucpropd 17241 homafval 17283 setcval 17331 catcval 17350 estrcval 17368 estrchomfeqhom 17380 hofval 17496 hofpropd 17511 islat 17651 istsr 17821 cnvtsr 17826 isdir 17836 tsrdir 17842 intopsn 17858 frmdval 18010 resgrpplusfrn 18111 opsrval 20249 matval 21014 ustval 22805 trust 22832 utop2nei 22853 utop3cls 22854 utopreg 22855 ussval 22862 ressuss 22866 tususs 22873 fmucnd 22895 cfilufg 22896 trcfilu 22897 neipcfilu 22899 ispsmet 22908 prdsdsf 22971 prdsxmet 22973 ressprdsds 22975 xpsdsfn2 22982 xpsxmetlem 22983 xpsmet 22986 isxms 23051 isms 23053 xmspropd 23077 mspropd 23078 setsxms 23083 setsms 23084 imasf1oxms 23093 imasf1oms 23094 ressxms 23129 ressms 23130 prdsxmslem2 23133 metuval 23153 nmpropd2 23198 ngppropd 23240 tngngp2 23255 pi1addf 23645 pi1addval 23646 iscms 23942 cmspropd 23946 cmssmscld 23947 cmsss 23948 cssbn 23972 rrxds 23990 rrxmfval 24003 minveclem3a 24024 dvlip2 24586 dchrval 25804 brcgr 26680 issh 28979 qtophaus 31095 prsssdm 31155 ordtrestNEW 31159 ordtrest2NEW 31161 isrrext 31236 sibfof 31593 satefv 32656 mdvval 32746 msrval 32780 mthmpps 32824 madeval 33284 funtransport 33487 fvtransport 33488 prdsbnd2 35067 cnpwstotbnd 35069 isrngo 35169 isrngod 35170 rngosn3 35196 isdivrngo 35222 drngoi 35223 isgrpda 35227 ldualset 36255 aomclem8 39654 intopval 44102 rngcvalALTV 44225 rngcval 44226 rnghmsubcsetclem1 44239 rngccat 44242 rngchomrnghmresALTV 44260 ringcvalALTV 44271 ringcval 44272 rhmsubcsetclem1 44285 ringccat 44288 rhmsubcrngclem1 44291 rhmsubcrngc 44293 srhmsubc 44340 rhmsubc 44354 srhmsubcALTV 44358 elpglem3 44808 |
Copyright terms: Public domain | W3C validator |