Theorem sqxpeqd 5708

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

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1, 1	xpeq12d 5707	1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵))

Syntax hints:   → wi 4   = wceq 1541   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5211  df-xp 5682

This theorem is referenced by:  xpcoid  6289  hartogslem1  9539  isfin6  10297  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwe2lem3  10630  fpwwe2lem7  10634  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwe2  10640  fpwwecbv  10641  fpwwelem  10642  canthwelem  10647  canthwe  10648  pwfseqlem4  10659  prdsval  17405  imasval  17461  imasaddfnlem  17478  comfffval  17646  comfeq  17654  oppcval  17661  sscfn1  17768  sscfn2  17769  isssc  17771  ssceq  17777  reschomf  17783  isfunc  17818  idfuval  17830  funcres  17850  funcpropd  17855  fucval  17914  fucpropd  17934  homafval  17983  setcval  18031  catcval  18054  estrcval  18079  estrchomfeqhom  18091  hofval  18209  hofpropd  18224  islat  18390  istsr  18540  cnvtsr  18545  isdir  18555  tsrdir  18561  intopsn  18579  frmdval  18768  resgrpplusfrn  18872  opsrval  21820  matval  22131  ustval  23927  trust  23954  utop2nei  23975  utop3cls  23976  utopreg  23977  ussval  23984  ressuss  23987  tususs  23995  fmucnd  24017  cfilufg  24018  trcfilu  24019  neipcfilu  24021  ispsmet  24030  prdsdsf  24093  prdsxmet  24095  ressprdsds  24097  xpsdsfn2  24104  xpsxmetlem  24105  xpsmet  24108  isxms  24173  isms  24175  xmspropd  24199  mspropd  24200  setsxms  24207  setsms  24208  imasf1oxms  24218  imasf1oms  24219  ressxms  24254  ressms  24255  prdsxmslem2  24258  metuval  24278  nmpropd2  24324  ngppropd  24366  tngngp2  24389  pi1addf  24787  pi1addval  24788  iscms  25086  cmspropd  25090  cmssmscld  25091  cmsss  25092  cssbn  25116  rrxds  25134  rrxmfval  25147  minveclem3a  25168  dvlip2  25736  dchrval  26961  madeval  27572  brcgr  28413  issh  30716  qtophaus  33102  prsssdm  33183  ordtrestNEW  33187  ordtrest2NEW  33189  isrrext  33266  sibfof  33625  satefv  34691  mdvval  34781  msrval  34815  mthmpps  34859  funtransport  35295  fvtransport  35296  prdsbnd2  36966  cnpwstotbnd  36968  isrngo  37068  isrngod  37069  rngosn3  37095  isdivrngo  37121  drngoi  37122  isgrpda  37126  ldualset  38298  aomclem8  42105  intopval  46879  rngcvalALTV  46948  rngcval  46949  rnghmsubcsetclem1  46962  rngccat  46965  rngchomrnghmresALTV  46983  ringcvalALTV  46994  ringcval  46995  rhmsubcsetclem1  47008  ringccat  47011  rhmsubcrngclem1  47014  rhmsubcrngc  47016  srhmsubc  47063  rhmsubc  47077  srhmsubcALTV  47081  elpglem3  47846  pgindnf  47849