Theorem sqxpeqd 5612

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-xp 5586

This theorem is referenced by:  xpcoid  6182  hartogslem1  9231  isfin6  9987  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwe2lem3  10320  fpwwe2lem7  10324  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  fpwwecbv  10331  fpwwelem  10332  canthwelem  10337  canthwe  10338  pwfseqlem4  10349  prdsval  17083  imasval  17139  imasaddfnlem  17156  comfffval  17324  comfeq  17332  oppcval  17339  sscfn1  17446  sscfn2  17447  isssc  17449  ssceq  17455  reschomf  17461  isfunc  17495  idfuval  17507  funcres  17527  funcpropd  17532  fucval  17591  fucpropd  17611  homafval  17660  setcval  17708  catcval  17731  estrcval  17756  estrchomfeqhom  17768  hofval  17886  hofpropd  17901  islat  18066  istsr  18216  cnvtsr  18221  isdir  18231  tsrdir  18237  intopsn  18253  frmdval  18405  resgrpplusfrn  18508  opsrval  21157  matval  21468  ustval  23262  trust  23289  utop2nei  23310  utop3cls  23311  utopreg  23312  ussval  23319  ressuss  23322  tususs  23330  fmucnd  23352  cfilufg  23353  trcfilu  23354  neipcfilu  23356  ispsmet  23365  prdsdsf  23428  prdsxmet  23430  ressprdsds  23432  xpsdsfn2  23439  xpsxmetlem  23440  xpsmet  23443  isxms  23508  isms  23510  xmspropd  23534  mspropd  23535  setsxms  23540  setsms  23541  imasf1oxms  23551  imasf1oms  23552  ressxms  23587  ressms  23588  prdsxmslem2  23591  metuval  23611  nmpropd2  23657  ngppropd  23699  tngngp2  23722  pi1addf  24116  pi1addval  24117  iscms  24414  cmspropd  24418  cmssmscld  24419  cmsss  24420  cssbn  24444  rrxds  24462  rrxmfval  24475  minveclem3a  24496  dvlip2  25064  dchrval  26287  brcgr  27171  issh  29471  qtophaus  31688  prsssdm  31769  ordtrestNEW  31773  ordtrest2NEW  31775  isrrext  31850  sibfof  32207  satefv  33276  mdvval  33366  msrval  33400  mthmpps  33444  madeval  33963  funtransport  34260  fvtransport  34261  prdsbnd2  35880  cnpwstotbnd  35882  isrngo  35982  isrngod  35983  rngosn3  36009  isdivrngo  36035  drngoi  36036  isgrpda  36040  ldualset  37066  aomclem8  40802  intopval  45284  rngcvalALTV  45407  rngcval  45408  rnghmsubcsetclem1  45421  rngccat  45424  rngchomrnghmresALTV  45442  ringcvalALTV  45453  ringcval  45454  rhmsubcsetclem1  45467  ringccat  45470  rhmsubcrngclem1  45473  rhmsubcrngc  45475  srhmsubc  45522  rhmsubc  45536  srhmsubcALTV  45540  elpglem3  46304