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

Theorem sqxpeqd 4939
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  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sqxpeqd  |-  ( ph  ->  ( A  X.  A
)  =  ( B  X.  B ) )

Proof of Theorem sqxpeqd
StepHypRef Expression
1 xpeq1d.1 . 2  |-  ( ph  ->  A  =  B )
21, 1xpeq12d 4938 1  |-  ( ph  ->  ( A  X.  A
)  =  ( B  X.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    X. cxp 4911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-opab 4426  df-xp 4919
This theorem is referenced by:  xpcoid  5457  hartogslem1  7882  isfin6  8593  fpwwe2cbv  8919  fpwwe2lem2  8921  fpwwe2lem3  8922  fpwwe2lem8  8926  fpwwe2lem12  8930  fpwwe2lem13  8931  fpwwe2  8932  fpwwecbv  8933  fpwwelem  8934  canthwelem  8939  canthwe  8940  pwfseqlem4  8951  prdsval  14862  imasval  14918  imasaddfnlem  14935  comfffval  15104  comfeq  15112  oppcval  15119  sscfn1  15223  sscfn2  15224  isssc  15226  ssceq  15232  reschomf  15237  isfunc  15270  idfuval  15282  funcres  15302  funcpropd  15306  fucval  15364  fucpropd  15383  homafval  15425  setcval  15473  catcval  15492  estrcval  15510  estrchomfeqhom  15522  hofval  15638  hofpropd  15653  islat  15794  istsr  15964  cnvtsr  15969  isdir  15979  tsrdir  15985  intopsn  15999  frmdval  16136  opsrval  18252  matval  18998  ustval  20790  trust  20817  utop2nei  20838  utop3cls  20839  utopreg  20840  ussval  20847  ressuss  20851  tususs  20858  fmucnd  20880  cfilufg  20881  trcfilu  20882  neipcfilu  20884  ispsmet  20893  prdsdsf  20955  prdsxmet  20957  ressprdsds  20959  xpsdsfn2  20966  xpsxmetlem  20967  xpsmet  20970  isxms  21035  isms  21037  xmspropd  21061  mspropd  21062  setsxms  21067  setsms  21068  imasf1oxms  21077  imasf1oms  21078  ressxms  21113  ressms  21114  prdsxmslem2  21117  metuval  21138  nmpropd2  21200  ngppropd  21236  tngngp2  21251  pi1addf  21632  pi1addval  21633  iscms  21869  cmspropd  21873  cmsss  21874  rrxds  21910  rrxmfval  21918  minveclem3a  21927  dvlip2  22481  dchrval  23626  brcgr  24324  isgrp2d  25354  isgrpda  25416  efghgrpOLD  25492  isrngo  25497  isrngod  25498  drngoi  25526  rngosn3  25545  isdivrngo  25550  issh  26242  qtophaus  27993  prsssdm  28053  ordtrestNEW  28057  ordtrest2NEW  28059  isrrext  28134  sibfof  28465  mdvval  29053  msrval  29087  mthmpps  29131  funtransport  29834  fvtransport  29835  prdsbnd2  30457  cnpwstotbnd  30459  aomclem8  31173  intopval  32844  rngcvalALTV  32969  rngcval  32970  rnghmsubcsetclem1  32983  rngccat  32986  rngchomrnghmresALTV  33004  ringcvalALTV  33015  ringcval  33016  rhmsubcsetclem1  33029  ringccat  33032  rhmsubcrngclem1  33035  rhmsubcrngc  33037  srhmsubc  33084  rhmsubc  33098  srhmsubcALTV  33103  bj-diagval  34953  ldualset  35263
  Copyright terms: Public domain W3C validator