Theorem sqxpeqd 5707

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 5706	1 ⊢ (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵))

Syntax hints:   → wi 4   = wceq 1539   × cxp 5673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-opab 5210  df-xp 5681

This theorem is referenced by:  xpcoid  6288  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  24794  pi1addval  24795  iscms  25093  cmspropd  25097  cmssmscld  25098  cmsss  25099  cssbn  25123  rrxds  25141  rrxmfval  25154  minveclem3a  25175  dvlip2  25747  dchrval  26973  madeval  27584  brcgr  28425  issh  30728  qtophaus  33114  prsssdm  33195  ordtrestNEW  33199  ordtrest2NEW  33201  isrrext  33278  sibfof  33637  satefv  34703  mdvval  34793  msrval  34827  mthmpps  34871  funtransport  35307  fvtransport  35308  prdsbnd2  36966  cnpwstotbnd  36968  isrngo  37068  isrngod  37069  rngosn3  37095  isdivrngo  37121  drngoi  37122  isgrpda  37126  ldualset  38298  aomclem8  42105  intopval  46878  rngcvalALTV  46947  rngcval  46948  rnghmsubcsetclem1  46961  rngccat  46964  rngchomrnghmresALTV  46982  ringcvalALTV  46993  ringcval  46994  rhmsubcsetclem1  47007  ringccat  47010  rhmsubcrngclem1  47013  rhmsubcrngc  47015  srhmsubc  47062  rhmsubc  47076  srhmsubcALTV  47080  elpglem3  47845  pgindnf  47848