Theorem sqxpeqd 5374

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

Syntax hints:   → wi 4   = wceq 1656   × cxp 5340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-opab 4936  df-xp 5348

This theorem is referenced by:  xpcoid  5917  hartogslem1  8716  isfin6  9437  fpwwe2cbv  9767  fpwwe2lem2  9769  fpwwe2lem3  9770  fpwwe2lem8  9774  fpwwe2lem12  9778  fpwwe2lem13  9779  fpwwe2  9780  fpwwecbv  9781  fpwwelem  9782  canthwelem  9787  canthwe  9788  pwfseqlem4  9799  prdsval  16468  imasval  16524  imasaddfnlem  16541  comfffval  16710  comfeq  16718  oppcval  16725  sscfn1  16829  sscfn2  16830  isssc  16832  ssceq  16838  reschomf  16843  isfunc  16876  idfuval  16888  funcres  16908  funcpropd  16912  fucval  16970  fucpropd  16989  homafval  17031  setcval  17079  catcval  17098  estrcval  17116  estrchomfeqhom  17128  hofval  17245  hofpropd  17260  islat  17400  istsr  17570  cnvtsr  17575  isdir  17585  tsrdir  17591  intopsn  17606  frmdval  17742  resgrpplusfrn  17790  opsrval  19835  matval  20584  ustval  22376  trust  22403  utop2nei  22424  utop3cls  22425  utopreg  22426  ussval  22433  ressuss  22437  tususs  22444  fmucnd  22466  cfilufg  22467  trcfilu  22468  neipcfilu  22470  ispsmet  22479  prdsdsf  22542  prdsxmet  22544  ressprdsds  22546  xpsdsfn2  22553  xpsxmetlem  22554  xpsmet  22557  isxms  22622  isms  22624  xmspropd  22648  mspropd  22649  setsxms  22654  setsms  22655  imasf1oxms  22664  imasf1oms  22665  ressxms  22700  ressms  22701  prdsxmslem2  22704  metuval  22724  nmpropd2  22769  ngppropd  22811  tngngp2  22826  pi1addf  23216  pi1addval  23217  iscms  23513  cmspropd  23517  cmssmscld  23518  cmsss  23519  cssbn  23543  rrxds  23561  rrxmfval  23574  minveclem3a  23595  dvlip2  24157  dchrval  25372  brcgr  26199  issh  28609  qtophaus  30437  prsssdm  30497  ordtrestNEW  30501  ordtrest2NEW  30503  isrrext  30578  sibfof  30936  mdvval  31936  msrval  31970  mthmpps  32014  madeval  32463  funtransport  32666  fvtransport  32667  bj-diagval  33612  prdsbnd2  34129  cnpwstotbnd  34131  isrngo  34231  isrngod  34232  rngosn3  34258  isdivrngo  34284  drngoi  34285  isgrpda  34289  ldualset  35193  aomclem8  38467  intopval  42678  rngcvalALTV  42801  rngcval  42802  rnghmsubcsetclem1  42815  rngccat  42818  rngchomrnghmresALTV  42836  ringcvalALTV  42847  ringcval  42848  rhmsubcsetclem1  42861  ringccat  42864  rhmsubcrngclem1  42867  rhmsubcrngc  42869  srhmsubc  42916  rhmsubc  42930  srhmsubcALTV  42934  elpglem3  43347