Theorem sqxpeqd 5732

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

Syntax hints:   → wi 4   = wceq 1537   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpcoid  6321  hartogslem1  9611  isfin6  10369  fpwwe2cbv  10699  fpwwe2lem2  10701  fpwwe2lem3  10702  fpwwe2lem4  10703  fpwwe2lem7  10706  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  fpwwecbv  10713  fpwwelem  10714  canthwelem  10719  canthwe  10720  pwfseqlem4  10731  prdsval  17515  imasval  17571  imasaddfnlem  17588  comfffval  17756  comfeq  17764  oppcval  17771  sscfn1  17878  sscfn2  17879  isssc  17881  ssceq  17887  reschomf  17893  isfunc  17928  idfuval  17940  funcres  17960  funcpropd  17967  fucval  18027  fucpropd  18047  homafval  18096  setcval  18144  catcval  18167  estrcval  18192  estrchomfeqhom  18204  hofval  18322  hofpropd  18337  islat  18503  istsr  18653  cnvtsr  18658  isdir  18668  tsrdir  18674  intopsn  18692  frmdval  18886  resgrpplusfrn  18990  rngcval  20640  rnghmsubcsetclem1  20653  rngccat  20656  ringcval  20669  rhmsubcsetclem1  20682  ringccat  20685  rhmsubcrngclem1  20688  rhmsubcrngc  20690  srhmsubc  20702  rhmsubc  20711  opsrval  22087  matval  22436  ustval  24232  trust  24259  utop2nei  24280  utop3cls  24281  utopreg  24282  ussval  24289  ressuss  24292  tususs  24300  fmucnd  24322  cfilufg  24323  trcfilu  24324  neipcfilu  24326  ispsmet  24335  prdsdsf  24398  prdsxmet  24400  ressprdsds  24402  xpsdsfn2  24409  xpsxmetlem  24410  xpsmet  24413  isxms  24478  isms  24480  xmspropd  24504  mspropd  24505  setsxms  24512  setsms  24513  imasf1oxms  24523  imasf1oms  24524  ressxms  24559  ressms  24560  prdsxmslem2  24563  metuval  24583  nmpropd2  24629  ngppropd  24671  tngngp2  24694  pi1addf  25099  pi1addval  25100  iscms  25398  cmspropd  25402  cmssmscld  25403  cmsss  25404  cssbn  25428  rrxds  25446  rrxmfval  25459  minveclem3a  25480  dvlip2  26054  dchrval  27296  madeval  27909  brcgr  28933  issh  31240  qtophaus  33782  prsssdm  33863  ordtrestNEW  33867  ordtrest2NEW  33869  isrrext  33946  sibfof  34305  satefv  35382  mdvval  35472  msrval  35506  mthmpps  35550  funtransport  35995  fvtransport  35996  prdsbnd2  37755  cnpwstotbnd  37757  isrngo  37857  isrngod  37858  rngosn3  37884  isdivrngo  37910  drngoi  37911  isgrpda  37915  ldualset  39081  aomclem8  43018  intopval  47925  rngcvalALTV  47988  rngchomrnghmresALTV  48002  ringcvalALTV  48012  srhmsubcALTV  48048  elpglem3  48805  pgindnf  48808