Theorem sqxpeqd 5654

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-opab 5159  df-xp 5628

This theorem is referenced by:  xpcoid  6246  hartogslem1  9445  isfin6  10208  fpwwe2cbv  10539  fpwwe2lem2  10541  fpwwe2lem3  10542  fpwwe2lem4  10543  fpwwe2lem7  10546  fpwwe2lem11  10550  fpwwe2lem12  10551  fpwwe2  10552  fpwwecbv  10553  fpwwelem  10554  canthwelem  10559  canthwe  10560  pwfseqlem4  10571  prdsval  17373  imasval  17430  imasaddfnlem  17447  comfffval  17619  comfeq  17627  oppcval  17634  sscfn1  17739  sscfn2  17740  isssc  17742  ssceq  17748  reschomf  17753  isfunc  17786  idfuval  17798  funcres  17818  funcpropd  17824  fucval  17883  fucpropd  17902  homafval  17951  setcval  17999  catcval  18022  estrcval  18045  estrchomfeqhom  18057  hofval  18173  hofpropd  18188  islat  18354  istsr  18504  cnvtsr  18509  isdir  18519  tsrdir  18525  intopsn  18577  frmdval  18774  resgrpplusfrn  18878  rngcval  20549  rnghmsubcsetclem1  20562  rngccat  20565  ringcval  20578  rhmsubcsetclem1  20591  ringccat  20594  rhmsubcrngclem1  20597  rhmsubcrngc  20599  srhmsubc  20611  rhmsubc  20620  opsrval  21999  matval  22353  ustval  24145  trust  24171  utop2nei  24192  utop3cls  24193  utopreg  24194  ussval  24201  ressuss  24204  tususs  24211  fmucnd  24233  cfilufg  24234  trcfilu  24235  neipcfilu  24237  ispsmet  24246  prdsdsf  24309  prdsxmet  24311  ressprdsds  24313  xpsdsfn2  24320  xpsxmetlem  24321  xpsmet  24324  isxms  24389  isms  24391  xmspropd  24415  mspropd  24416  setsxms  24421  setsms  24422  imasf1oxms  24431  imasf1oms  24432  ressxms  24467  ressms  24468  prdsxmslem2  24471  metuval  24491  nmpropd2  24537  ngppropd  24579  tngngp2  24594  pi1addf  25001  pi1addval  25002  iscms  25299  cmspropd  25303  cmssmscld  25304  cmsss  25305  cssbn  25329  rrxds  25347  rrxmfval  25360  minveclem3a  25381  dvlip2  25954  dchrval  27199  madeval  27820  brcgr  28922  issh  31232  qtophaus  33942  prsssdm  34023  ordtrestNEW  34027  ordtrest2NEW  34029  isrrext  34106  sibfof  34446  satefv  35557  mdvval  35647  msrval  35681  mthmpps  35725  funtransport  36174  fvtransport  36175  prdsbnd2  37935  cnpwstotbnd  37937  isrngo  38037  isrngod  38038  rngosn3  38064  isdivrngo  38090  drngoi  38091  isgrpda  38095  ldualset  39324  aomclem8  43245  intopval  48390  rngcvalALTV  48453  rngchomrnghmresALTV  48467  ringcvalALTV  48477  srhmsubcALTV  48513  nelsubc3lem  49257  0funcg2  49271  imaidfu2  49298  idfullsubc  49348  termcfuncval  49719  cnelsubclem  49790  elpglem3  49900  pgindnf  49903