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

Theorem sqxpeqd 5052
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 5051 1 (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   × cxp 5023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-opab 4635  df-xp 5031
This theorem is referenced by:  xpcoid  5576  hartogslem1  8304  isfin6  8979  fpwwe2cbv  9305  fpwwe2lem2  9307  fpwwe2lem3  9308  fpwwe2lem8  9312  fpwwe2lem12  9316  fpwwe2lem13  9317  fpwwe2  9318  fpwwecbv  9319  fpwwelem  9320  canthwelem  9325  canthwe  9326  pwfseqlem4  9337  prdsval  15881  imasval  15937  imasaddfnlem  15954  comfffval  16124  comfeq  16132  oppcval  16139  sscfn1  16243  sscfn2  16244  isssc  16246  ssceq  16252  reschomf  16257  isfunc  16290  idfuval  16302  funcres  16322  funcpropd  16326  fucval  16384  fucpropd  16403  homafval  16445  setcval  16493  catcval  16512  estrcval  16530  estrchomfeqhom  16542  hofval  16658  hofpropd  16673  islat  16813  istsr  16983  cnvtsr  16988  isdir  16998  tsrdir  17004  intopsn  17019  frmdval  17154  resgrpplusfrn  17202  opsrval  19238  matval  19975  ustval  21755  trust  21782  utop2nei  21803  utop3cls  21804  utopreg  21805  ussval  21812  ressuss  21816  tususs  21823  fmucnd  21845  cfilufg  21846  trcfilu  21847  neipcfilu  21849  ispsmet  21858  prdsdsf  21920  prdsxmet  21922  ressprdsds  21924  xpsdsfn2  21931  xpsxmetlem  21932  xpsmet  21935  isxms  22000  isms  22002  xmspropd  22026  mspropd  22027  setsxms  22032  setsms  22033  imasf1oxms  22042  imasf1oms  22043  ressxms  22078  ressms  22079  prdsxmslem2  22082  metuval  22102  nmpropd2  22147  ngppropd  22186  tngngp2  22201  pi1addf  22583  pi1addval  22584  iscms  22864  cmspropd  22868  cmsss  22869  rrxds  22903  rrxmfval  22911  minveclem3a  22920  dvlip2  23476  dchrval  24673  brcgr  25495  issh  27252  qtophaus  29034  prsssdm  29094  ordtrestNEW  29098  ordtrest2NEW  29100  isrrext  29175  sibfof  29532  mdvval  30458  msrval  30492  mthmpps  30536  funtransport  31111  fvtransport  31112  bj-diagval  32067  prdsbnd2  32564  cnpwstotbnd  32566  isrngo  32666  isrngod  32667  rngosn3  32693  isdivrngo  32719  drngoi  32720  isgrpda  32724  ldualset  33230  aomclem8  36449  intopval  41627  rngcvalALTV  41752  rngcval  41753  rnghmsubcsetclem1  41766  rngccat  41769  rngchomrnghmresALTV  41787  ringcvalALTV  41798  ringcval  41799  rhmsubcsetclem1  41812  ringccat  41815  rhmsubcrngclem1  41818  rhmsubcrngc  41820  srhmsubc  41867  rhmsubc  41881  srhmsubcALTV  41886
  Copyright terms: Public domain W3C validator