Theorem sqxpeqd 5551

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

Syntax hints:   → wi 4   = wceq 1538   × cxp 5517

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5093  df-xp 5525

This theorem is referenced by:  xpcoid  6109  hartogslem1  8990  isfin6  9711  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwe2lem3  10044  fpwwe2lem8  10048  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  fpwwecbv  10055  fpwwelem  10056  canthwelem  10061  canthwe  10062  pwfseqlem4  10073  prdsval  16720  imasval  16776  imasaddfnlem  16793  comfffval  16960  comfeq  16968  oppcval  16975  sscfn1  17079  sscfn2  17080  isssc  17082  ssceq  17088  reschomf  17093  isfunc  17126  idfuval  17138  funcres  17158  funcpropd  17162  fucval  17220  fucpropd  17239  homafval  17281  setcval  17329  catcval  17348  estrcval  17366  estrchomfeqhom  17378  hofval  17494  hofpropd  17509  islat  17649  istsr  17819  cnvtsr  17824  isdir  17834  tsrdir  17840  intopsn  17856  frmdval  18008  resgrpplusfrn  18109  opsrval  20714  matval  21016  ustval  22808  trust  22835  utop2nei  22856  utop3cls  22857  utopreg  22858  ussval  22865  ressuss  22869  tususs  22876  fmucnd  22898  cfilufg  22899  trcfilu  22900  neipcfilu  22902  ispsmet  22911  prdsdsf  22974  prdsxmet  22976  ressprdsds  22978  xpsdsfn2  22985  xpsxmetlem  22986  xpsmet  22989  isxms  23054  isms  23056  xmspropd  23080  mspropd  23081  setsxms  23086  setsms  23087  imasf1oxms  23096  imasf1oms  23097  ressxms  23132  ressms  23133  prdsxmslem2  23136  metuval  23156  nmpropd2  23201  ngppropd  23243  tngngp2  23258  pi1addf  23652  pi1addval  23653  iscms  23949  cmspropd  23953  cmssmscld  23954  cmsss  23955  cssbn  23979  rrxds  23997  rrxmfval  24010  minveclem3a  24031  dvlip2  24598  dchrval  25818  brcgr  26694  issh  28991  qtophaus  31189  prsssdm  31270  ordtrestNEW  31274  ordtrest2NEW  31276  isrrext  31351  sibfof  31708  satefv  32774  mdvval  32864  msrval  32898  mthmpps  32942  madeval  33402  funtransport  33605  fvtransport  33606  prdsbnd2  35233  cnpwstotbnd  35235  isrngo  35335  isrngod  35336  rngosn3  35362  isdivrngo  35388  drngoi  35389  isgrpda  35393  ldualset  36421  aomclem8  40005  intopval  44462  rngcvalALTV  44585  rngcval  44586  rnghmsubcsetclem1  44599  rngccat  44602  rngchomrnghmresALTV  44620  ringcvalALTV  44631  ringcval  44632  rhmsubcsetclem1  44645  ringccat  44648  rhmsubcrngclem1  44651  rhmsubcrngc  44653  srhmsubc  44700  rhmsubc  44714  srhmsubcALTV  44718  elpglem3  45242