Theorem sqxpeqd 5710

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

Syntax hints:   → wi 4   = wceq 1534   × cxp 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-opab 5211  df-xp 5684

This theorem is referenced by:  xpcoid  6294  hartogslem1  9565  isfin6  10323  fpwwe2cbv  10653  fpwwe2lem2  10655  fpwwe2lem3  10656  fpwwe2lem7  10660  fpwwe2lem11  10664  fpwwe2lem12  10665  fpwwe2  10666  fpwwecbv  10667  fpwwelem  10668  canthwelem  10673  canthwe  10674  pwfseqlem4  10685  prdsval  17436  imasval  17492  imasaddfnlem  17509  comfffval  17677  comfeq  17685  oppcval  17692  sscfn1  17799  sscfn2  17800  isssc  17802  ssceq  17808  reschomf  17814  isfunc  17849  idfuval  17861  funcres  17881  funcpropd  17888  fucval  17948  fucpropd  17968  homafval  18017  setcval  18065  catcval  18088  estrcval  18113  estrchomfeqhom  18125  hofval  18243  hofpropd  18258  islat  18424  istsr  18574  cnvtsr  18579  isdir  18589  tsrdir  18595  intopsn  18613  frmdval  18802  resgrpplusfrn  18906  rngcval  20550  rnghmsubcsetclem1  20563  rngccat  20566  ringcval  20579  rhmsubcsetclem1  20592  ringccat  20595  rhmsubcrngclem1  20598  rhmsubcrngc  20600  srhmsubc  20612  rhmsubc  20621  opsrval  21983  matval  22310  ustval  24106  trust  24133  utop2nei  24154  utop3cls  24155  utopreg  24156  ussval  24163  ressuss  24166  tususs  24174  fmucnd  24196  cfilufg  24197  trcfilu  24198  neipcfilu  24200  ispsmet  24209  prdsdsf  24272  prdsxmet  24274  ressprdsds  24276  xpsdsfn2  24283  xpsxmetlem  24284  xpsmet  24287  isxms  24352  isms  24354  xmspropd  24378  mspropd  24379  setsxms  24386  setsms  24387  imasf1oxms  24397  imasf1oms  24398  ressxms  24433  ressms  24434  prdsxmslem2  24437  metuval  24457  nmpropd2  24503  ngppropd  24545  tngngp2  24568  pi1addf  24973  pi1addval  24974  iscms  25272  cmspropd  25276  cmssmscld  25277  cmsss  25278  cssbn  25302  rrxds  25320  rrxmfval  25333  minveclem3a  25354  dvlip2  25927  dchrval  27166  madeval  27778  brcgr  28710  issh  31017  qtophaus  33437  prsssdm  33518  ordtrestNEW  33522  ordtrest2NEW  33524  isrrext  33601  sibfof  33960  satefv  35024  mdvval  35114  msrval  35148  mthmpps  35192  funtransport  35627  fvtransport  35628  prdsbnd2  37268  cnpwstotbnd  37270  isrngo  37370  isrngod  37371  rngosn3  37397  isdivrngo  37423  drngoi  37424  isgrpda  37428  ldualset  38597  aomclem8  42485  intopval  47264  rngcvalALTV  47327  rngchomrnghmresALTV  47341  ringcvalALTV  47351  srhmsubcALTV  47387  elpglem3  48144  pgindnf  48147