Theorem sqxpeqd 5651

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

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

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 5155  df-xp 5625

This theorem is referenced by:  xpcoid  6238  hartogslem1  9434  isfin6  10194  fpwwe2cbv  10524  fpwwe2lem2  10526  fpwwe2lem3  10527  fpwwe2lem4  10528  fpwwe2lem7  10531  fpwwe2lem11  10535  fpwwe2lem12  10536  fpwwe2  10537  fpwwecbv  10538  fpwwelem  10539  canthwelem  10544  canthwe  10545  pwfseqlem4  10556  prdsval  17359  imasval  17415  imasaddfnlem  17432  comfffval  17604  comfeq  17612  oppcval  17619  sscfn1  17724  sscfn2  17725  isssc  17727  ssceq  17733  reschomf  17738  isfunc  17771  idfuval  17783  funcres  17803  funcpropd  17809  fucval  17868  fucpropd  17887  homafval  17936  setcval  17984  catcval  18007  estrcval  18030  estrchomfeqhom  18042  hofval  18158  hofpropd  18173  islat  18339  istsr  18489  cnvtsr  18494  isdir  18504  tsrdir  18510  intopsn  18528  frmdval  18725  resgrpplusfrn  18829  rngcval  20503  rnghmsubcsetclem1  20516  rngccat  20519  ringcval  20532  rhmsubcsetclem1  20545  ringccat  20548  rhmsubcrngclem1  20551  rhmsubcrngc  20553  srhmsubc  20565  rhmsubc  20574  opsrval  21951  matval  22296  ustval  24088  trust  24115  utop2nei  24136  utop3cls  24137  utopreg  24138  ussval  24145  ressuss  24148  tususs  24155  fmucnd  24177  cfilufg  24178  trcfilu  24179  neipcfilu  24181  ispsmet  24190  prdsdsf  24253  prdsxmet  24255  ressprdsds  24257  xpsdsfn2  24264  xpsxmetlem  24265  xpsmet  24268  isxms  24333  isms  24335  xmspropd  24359  mspropd  24360  setsxms  24365  setsms  24366  imasf1oxms  24375  imasf1oms  24376  ressxms  24411  ressms  24412  prdsxmslem2  24415  metuval  24435  nmpropd2  24481  ngppropd  24523  tngngp2  24538  pi1addf  24945  pi1addval  24946  iscms  25243  cmspropd  25247  cmssmscld  25248  cmsss  25249  cssbn  25273  rrxds  25291  rrxmfval  25304  minveclem3a  25325  dvlip2  25898  dchrval  27143  madeval  27762  brcgr  28845  issh  31152  qtophaus  33809  prsssdm  33890  ordtrestNEW  33894  ordtrest2NEW  33896  isrrext  33973  sibfof  34314  satefv  35397  mdvval  35487  msrval  35521  mthmpps  35565  funtransport  36015  fvtransport  36016  prdsbnd2  37785  cnpwstotbnd  37787  isrngo  37887  isrngod  37888  rngosn3  37914  isdivrngo  37940  drngoi  37941  isgrpda  37945  ldualset  39114  aomclem8  43044  intopval  48196  rngcvalALTV  48259  rngchomrnghmresALTV  48273  ringcvalALTV  48283  srhmsubcALTV  48319  nelsubc3lem  49065  0funcg2  49079  imaidfu2  49106  idfullsubc  49156  termcfuncval  49527  cnelsubclem  49598  elpglem3  49708  pgindnf  49711