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

Theorem sqxpeqd 5131
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 5130 1 (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481   × cxp 5102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-opab 4704  df-xp 5110
This theorem is referenced by:  xpcoid  5664  hartogslem1  8432  isfin6  9107  fpwwe2cbv  9437  fpwwe2lem2  9439  fpwwe2lem3  9440  fpwwe2lem8  9444  fpwwe2lem12  9448  fpwwe2lem13  9449  fpwwe2  9450  fpwwecbv  9451  fpwwelem  9452  canthwelem  9457  canthwe  9458  pwfseqlem4  9469  prdsval  16096  imasval  16152  imasaddfnlem  16169  comfffval  16339  comfeq  16347  oppcval  16354  sscfn1  16458  sscfn2  16459  isssc  16461  ssceq  16467  reschomf  16472  isfunc  16505  idfuval  16517  funcres  16537  funcpropd  16541  fucval  16599  fucpropd  16618  homafval  16660  setcval  16708  catcval  16727  estrcval  16745  estrchomfeqhom  16757  hofval  16873  hofpropd  16888  islat  17028  istsr  17198  cnvtsr  17203  isdir  17213  tsrdir  17219  intopsn  17234  frmdval  17369  resgrpplusfrn  17417  opsrval  19455  matval  20198  ustval  21987  trust  22014  utop2nei  22035  utop3cls  22036  utopreg  22037  ussval  22044  ressuss  22048  tususs  22055  fmucnd  22077  cfilufg  22078  trcfilu  22079  neipcfilu  22081  ispsmet  22090  prdsdsf  22153  prdsxmet  22155  ressprdsds  22157  xpsdsfn2  22164  xpsxmetlem  22165  xpsmet  22168  isxms  22233  isms  22235  xmspropd  22259  mspropd  22260  setsxms  22265  setsms  22266  imasf1oxms  22275  imasf1oms  22276  ressxms  22311  ressms  22312  prdsxmslem2  22315  metuval  22335  nmpropd2  22380  ngppropd  22422  tngngp2  22437  pi1addf  22828  pi1addval  22829  iscms  23123  cmspropd  23127  cmsss  23128  rrxds  23162  rrxmfval  23170  minveclem3a  23179  dvlip2  23739  dchrval  24940  brcgr  25761  issh  28035  qtophaus  29877  prsssdm  29937  ordtrestNEW  29941  ordtrest2NEW  29943  isrrext  30018  sibfof  30376  mdvval  31375  msrval  31409  mthmpps  31453  madeval  31909  funtransport  32113  fvtransport  32114  bj-diagval  33061  prdsbnd2  33565  cnpwstotbnd  33567  isrngo  33667  isrngod  33668  rngosn3  33694  isdivrngo  33720  drngoi  33721  isgrpda  33725  ldualset  34231  aomclem8  37450  intopval  41603  rngcvalALTV  41726  rngcval  41727  rnghmsubcsetclem1  41740  rngccat  41743  rngchomrnghmresALTV  41761  ringcvalALTV  41772  ringcval  41773  rhmsubcsetclem1  41786  ringccat  41789  rhmsubcrngclem1  41792  rhmsubcrngc  41794  srhmsubc  41841  rhmsubc  41855  srhmsubcALTV  41859  elpglem3  42221
  Copyright terms: Public domain W3C validator