Theorem sqxpeqd 5663

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5165  df-xp 5637

This theorem is referenced by:  xpcoid  6251  hartogslem1  9471  isfin6  10229  fpwwe2cbv  10559  fpwwe2lem2  10561  fpwwe2lem3  10562  fpwwe2lem4  10563  fpwwe2lem7  10566  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwe2  10572  fpwwecbv  10573  fpwwelem  10574  canthwelem  10579  canthwe  10580  pwfseqlem4  10591  prdsval  17394  imasval  17450  imasaddfnlem  17467  comfffval  17639  comfeq  17647  oppcval  17654  sscfn1  17759  sscfn2  17760  isssc  17762  ssceq  17768  reschomf  17773  isfunc  17806  idfuval  17818  funcres  17838  funcpropd  17844  fucval  17903  fucpropd  17922  homafval  17971  setcval  18019  catcval  18042  estrcval  18065  estrchomfeqhom  18077  hofval  18193  hofpropd  18208  islat  18374  istsr  18524  cnvtsr  18529  isdir  18539  tsrdir  18545  intopsn  18563  frmdval  18760  resgrpplusfrn  18864  rngcval  20538  rnghmsubcsetclem1  20551  rngccat  20554  ringcval  20567  rhmsubcsetclem1  20580  ringccat  20583  rhmsubcrngclem1  20586  rhmsubcrngc  20588  srhmsubc  20600  rhmsubc  20609  opsrval  21986  matval  22331  ustval  24123  trust  24150  utop2nei  24171  utop3cls  24172  utopreg  24173  ussval  24180  ressuss  24183  tususs  24190  fmucnd  24212  cfilufg  24213  trcfilu  24214  neipcfilu  24216  ispsmet  24225  prdsdsf  24288  prdsxmet  24290  ressprdsds  24292  xpsdsfn2  24299  xpsxmetlem  24300  xpsmet  24303  isxms  24368  isms  24370  xmspropd  24394  mspropd  24395  setsxms  24400  setsms  24401  imasf1oxms  24410  imasf1oms  24411  ressxms  24446  ressms  24447  prdsxmslem2  24450  metuval  24470  nmpropd2  24516  ngppropd  24558  tngngp2  24573  pi1addf  24980  pi1addval  24981  iscms  25278  cmspropd  25282  cmssmscld  25283  cmsss  25284  cssbn  25308  rrxds  25326  rrxmfval  25339  minveclem3a  25360  dvlip2  25933  dchrval  27178  madeval  27797  brcgr  28880  issh  31187  qtophaus  33819  prsssdm  33900  ordtrestNEW  33904  ordtrest2NEW  33906  isrrext  33983  sibfof  34324  satefv  35394  mdvval  35484  msrval  35518  mthmpps  35562  funtransport  36012  fvtransport  36013  prdsbnd2  37782  cnpwstotbnd  37784  isrngo  37884  isrngod  37885  rngosn3  37911  isdivrngo  37937  drngoi  37938  isgrpda  37942  ldualset  39111  aomclem8  43043  intopval  48183  rngcvalALTV  48246  rngchomrnghmresALTV  48260  ringcvalALTV  48270  srhmsubcALTV  48306  nelsubc3lem  49052  0funcg2  49066  imaidfu2  49093  idfullsubc  49143  termcfuncval  49514  cnelsubclem  49585  elpglem3  49695  pgindnf  49698