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

Theorem sqxpeqd 4880
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 4879 1  |-  ( ph  ->  ( A  X.  A
)  =  ( B  X.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    X. cxp 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-opab 4485  df-xp 4860
This theorem is referenced by:  xpcoid  5397  hartogslem1  8057  isfin6  8728  fpwwe2cbv  9054  fpwwe2lem2  9056  fpwwe2lem3  9057  fpwwe2lem8  9061  fpwwe2lem12  9065  fpwwe2lem13  9066  fpwwe2  9067  fpwwecbv  9068  fpwwelem  9069  canthwelem  9074  canthwe  9075  pwfseqlem4  9086  prdsval  15312  imasval  15368  imasaddfnlem  15385  comfffval  15554  comfeq  15562  oppcval  15569  sscfn1  15673  sscfn2  15674  isssc  15676  ssceq  15682  reschomf  15687  isfunc  15720  idfuval  15732  funcres  15752  funcpropd  15756  fucval  15814  fucpropd  15833  homafval  15875  setcval  15923  catcval  15942  estrcval  15960  estrchomfeqhom  15972  hofval  16088  hofpropd  16103  islat  16244  istsr  16414  cnvtsr  16419  isdir  16429  tsrdir  16435  intopsn  16449  frmdval  16586  opsrval  18633  matval  19367  ustval  21148  trust  21175  utop2nei  21196  utop3cls  21197  utopreg  21198  ussval  21205  ressuss  21209  tususs  21216  fmucnd  21238  cfilufg  21239  trcfilu  21240  neipcfilu  21242  ispsmet  21251  prdsdsf  21313  prdsxmet  21315  ressprdsds  21317  xpsdsfn2  21324  xpsxmetlem  21325  xpsmet  21328  isxms  21393  isms  21395  xmspropd  21419  mspropd  21420  setsxms  21425  setsms  21426  imasf1oxms  21435  imasf1oms  21436  ressxms  21471  ressms  21472  prdsxmslem2  21475  metuval  21495  nmpropd2  21540  ngppropd  21576  tngngp2  21591  pi1addf  21971  pi1addval  21972  iscms  22206  cmspropd  22210  cmsss  22211  rrxds  22245  rrxmfval  22253  minveclem3a  22262  dvlip2  22824  dchrval  24025  brcgr  24776  isgrp2d  25808  isgrpda  25870  efghgrpOLD  25946  isrngo  25951  isrngod  25952  drngoi  25980  rngosn3  25999  isdivrngo  26004  issh  26696  qtophaus  28502  prsssdm  28562  ordtrestNEW  28566  ordtrest2NEW  28568  isrrext  28643  sibfof  29001  mdvval  29930  msrval  29964  mthmpps  30008  funtransport  30583  fvtransport  30584  bj-diagval  31390  prdsbnd2  31830  cnpwstotbnd  31832  ldualset  32399  aomclem8  35624  intopval  38595  rngcvalALTV  38720  rngcval  38721  rnghmsubcsetclem1  38734  rngccat  38737  rngchomrnghmresALTV  38755  ringcvalALTV  38766  ringcval  38767  rhmsubcsetclem1  38780  ringccat  38783  rhmsubcrngclem1  38786  rhmsubcrngc  38788  srhmsubc  38835  rhmsubc  38849  srhmsubcALTV  38854
  Copyright terms: Public domain W3C validator