Theorem sqxpeqd 5666

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

Syntax hints:   → wi 4   = wceq 1542   × cxp 5632

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-xp 5640

This theorem is referenced by:  xpcoid  6258  hartogslem1  9461  isfin6  10224  fpwwe2cbv  10555  fpwwe2lem2  10557  fpwwe2lem3  10558  fpwwe2lem4  10559  fpwwe2lem7  10562  fpwwe2lem11  10566  fpwwe2lem12  10567  fpwwe2  10568  fpwwecbv  10569  fpwwelem  10570  canthwelem  10575  canthwe  10576  pwfseqlem4  10587  prdsval  17389  imasval  17446  imasaddfnlem  17463  comfffval  17635  comfeq  17643  oppcval  17650  sscfn1  17755  sscfn2  17756  isssc  17758  ssceq  17764  reschomf  17769  isfunc  17802  idfuval  17814  funcres  17834  funcpropd  17840  fucval  17899  fucpropd  17918  homafval  17967  setcval  18015  catcval  18038  estrcval  18061  estrchomfeqhom  18073  hofval  18189  hofpropd  18204  islat  18370  istsr  18520  cnvtsr  18525  isdir  18535  tsrdir  18541  intopsn  18593  frmdval  18790  resgrpplusfrn  18897  rngcval  20568  rnghmsubcsetclem1  20581  rngccat  20584  ringcval  20597  rhmsubcsetclem1  20610  ringccat  20613  rhmsubcrngclem1  20616  rhmsubcrngc  20618  srhmsubc  20630  rhmsubc  20639  opsrval  22018  matval  22372  ustval  24164  trust  24190  utop2nei  24211  utop3cls  24212  utopreg  24213  ussval  24220  ressuss  24223  tususs  24230  fmucnd  24252  cfilufg  24253  trcfilu  24254  neipcfilu  24256  ispsmet  24265  prdsdsf  24328  prdsxmet  24330  ressprdsds  24332  xpsdsfn2  24339  xpsxmetlem  24340  xpsmet  24343  isxms  24408  isms  24410  xmspropd  24434  mspropd  24435  setsxms  24440  setsms  24441  imasf1oxms  24450  imasf1oms  24451  ressxms  24486  ressms  24487  prdsxmslem2  24490  metuval  24510  nmpropd2  24556  ngppropd  24598  tngngp2  24613  pi1addf  25020  pi1addval  25021  iscms  25318  cmspropd  25322  cmssmscld  25323  cmsss  25324  cssbn  25348  rrxds  25366  rrxmfval  25379  minveclem3a  25400  dvlip2  25973  dchrval  27218  madeval  27845  brcgr  28991  issh  31302  qtophaus  34020  prsssdm  34101  ordtrestNEW  34105  ordtrest2NEW  34107  isrrext  34184  sibfof  34524  satefv  35636  mdvval  35726  msrval  35760  mthmpps  35804  funtransport  36253  fvtransport  36254  prdsbnd2  38075  cnpwstotbnd  38077  isrngo  38177  isrngod  38178  rngosn3  38204  isdivrngo  38230  drngoi  38231  isgrpda  38235  ldualset  39530  aomclem8  43447  intopval  48591  rngcvalALTV  48654  rngchomrnghmresALTV  48668  ringcvalALTV  48678  srhmsubcALTV  48714  nelsubc3lem  49458  0funcg2  49472  imaidfu2  49499  idfullsubc  49549  termcfuncval  49920  cnelsubclem  49991  elpglem3  50101  pgindnf  50104