Theorem sqxpeqd 5653

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

Syntax hints:   → wi 4   = wceq 1548   × cxp 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-opab 5138  df-xp 5627

This theorem is referenced by:  xpcoid  6245  hartogslem1  9451  isfin6  10217  fpwwe2cbv  10548  fpwwe2lem2  10550  fpwwe2lem3  10551  fpwwe2lem4  10552  fpwwe2lem7  10555  fpwwe2lem11  10559  fpwwe2lem12  10560  fpwwe2  10561  fpwwecbv  10562  fpwwelem  10563  canthwelem  10568  canthwe  10569  pwfseqlem4  10580  prdsval  17413  imasval  17470  imasaddfnlem  17487  comfffval  17659  comfeq  17667  oppcval  17674  sscfn1  17779  sscfn2  17780  isssc  17782  ssceq  17788  reschomf  17793  isfunc  17826  idfuval  17838  funcres  17858  funcpropd  17864  fucval  17923  fucpropd  17942  homafval  17991  setcval  18039  catcval  18062  estrcval  18085  estrchomfeqhom  18097  hofval  18213  hofpropd  18228  islat  18394  istsr  18544  cnvtsr  18549  isdir  18559  tsrdir  18565  intopsn  18617  frmdval  18814  resgrpplusfrn  18921  rngcval  20594  rnghmsubcsetclem1  20607  rngccat  20610  ringcval  20623  rhmsubcsetclem1  20636  ringccat  20639  rhmsubcrngclem1  20642  rhmsubcrngc  20644  srhmsubc  20656  rhmsubc  20665  opsrval  22026  matval  22398  ustval  24190  trust  24216  utop2nei  24237  utop3cls  24238  utopreg  24239  ussval  24246  ressuss  24249  tususs  24256  fmucnd  24278  cfilufg  24279  trcfilu  24280  neipcfilu  24282  ispsmet  24291  prdsdsf  24354  prdsxmet  24356  ressprdsds  24358  xpsdsfn2  24365  xpsxmetlem  24366  xpsmet  24369  isxms  24434  isms  24436  xmspropd  24460  mspropd  24461  setsxms  24466  setsms  24467  imasf1oxms  24476  imasf1oms  24477  ressxms  24512  ressms  24513  prdsxmslem2  24516  metuval  24536  nmpropd2  24582  ngppropd  24624  tngngp2  24639  pi1addf  25036  pi1addval  25037  iscms  25334  cmspropd  25338  cmssmscld  25339  cmsss  25340  cssbn  25364  rrxds  25382  rrxmfval  25395  minveclem3a  25416  dvlip2  25984  dchrval  27219  madeval  27846  brcgr  28991  issh  31301  qtophaus  34032  prsssdm  34113  ordtrestNEW  34117  ordtrest2NEW  34119  isrrext  34196  sibfof  34536  satefv  35657  mdvval  35747  msrval  35781  mthmpps  35825  funtransport  36274  fvtransport  36275  prdsbnd2  38177  cnpwstotbnd  38179  isrngo  38279  isrngod  38280  rngosn3  38306  isdivrngo  38332  drngoi  38333  isgrpda  38337  ldualset  39632  aomclem8  43521  intopval  48707  rngcvalALTV  48770  rngchomrnghmresALTV  48784  ringcvalALTV  48794  srhmsubcALTV  48830  nelsubc3lem  49574  0funcg2  49588  imaidfu2  49615  idfullsubc  49665  termcfuncval  50036  cnelsubclem  50107  elpglem3  50217  pgindnf  50220