MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sqxpeqd Structured version   Visualization version   GIF version

Theorem sqxpeqd 5586
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.)
Hypothesis
Ref Expression
xpeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sqxpeqd (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵))

Proof of Theorem sqxpeqd
StepHypRef Expression
1 xpeq1d.1 . 2 (𝜑𝐴 = 𝐵)
21, 1xpeq12d 5585 1 (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530   × cxp 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-opab 5126  df-xp 5560
This theorem is referenced by:  xpcoid  6139  hartogslem1  8995  isfin6  9711  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwe2lem3  10044  fpwwe2lem8  10048  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  fpwwecbv  10055  fpwwelem  10056  canthwelem  10061  canthwe  10062  pwfseqlem4  10073  prdsval  16718  imasval  16774  imasaddfnlem  16791  comfffval  16958  comfeq  16966  oppcval  16973  sscfn1  17077  sscfn2  17078  isssc  17080  ssceq  17086  reschomf  17091  isfunc  17124  idfuval  17136  funcres  17156  funcpropd  17160  fucval  17218  fucpropd  17237  homafval  17279  setcval  17327  catcval  17346  estrcval  17364  estrchomfeqhom  17376  hofval  17492  hofpropd  17507  islat  17647  istsr  17817  cnvtsr  17822  isdir  17832  tsrdir  17838  intopsn  17853  frmdval  17999  resgrpplusfrn  18047  opsrval  20174  matval  20939  ustval  22729  trust  22756  utop2nei  22777  utop3cls  22778  utopreg  22779  ussval  22786  ressuss  22790  tususs  22797  fmucnd  22819  cfilufg  22820  trcfilu  22821  neipcfilu  22823  ispsmet  22832  prdsdsf  22895  prdsxmet  22897  ressprdsds  22899  xpsdsfn2  22906  xpsxmetlem  22907  xpsmet  22910  isxms  22975  isms  22977  xmspropd  23001  mspropd  23002  setsxms  23007  setsms  23008  imasf1oxms  23017  imasf1oms  23018  ressxms  23053  ressms  23054  prdsxmslem2  23057  metuval  23077  nmpropd2  23122  ngppropd  23164  tngngp2  23179  pi1addf  23569  pi1addval  23570  iscms  23866  cmspropd  23870  cmssmscld  23871  cmsss  23872  cssbn  23896  rrxds  23914  rrxmfval  23927  minveclem3a  23948  dvlip2  24510  dchrval  25727  brcgr  26603  issh  28902  qtophaus  30989  prsssdm  31049  ordtrestNEW  31053  ordtrest2NEW  31055  isrrext  31130  sibfof  31487  satefv  32548  mdvval  32638  msrval  32672  mthmpps  32716  madeval  33176  funtransport  33379  fvtransport  33380  prdsbnd2  34944  cnpwstotbnd  34946  isrngo  35046  isrngod  35047  rngosn3  35073  isdivrngo  35099  drngoi  35100  isgrpda  35104  ldualset  36131  aomclem8  39529  intopval  43944  rngcvalALTV  44067  rngcval  44068  rnghmsubcsetclem1  44081  rngccat  44084  rngchomrnghmresALTV  44102  ringcvalALTV  44113  ringcval  44114  rhmsubcsetclem1  44127  ringccat  44130  rhmsubcrngclem1  44133  rhmsubcrngc  44135  srhmsubc  44182  rhmsubc  44196  srhmsubcALTV  44200  elpglem3  44650
  Copyright terms: Public domain W3C validator