Theorem sqxpeqd 5681

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

Syntax hints:   → wi 4   = wceq 1562   × cxp 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-opab 5165  df-xp 5655

This theorem is referenced by:  xpcoid  6279  hartogslem1  9492  isfin6  10259  fpwwe2cbv  10590  fpwwe2lem2  10592  fpwwe2lem3  10593  fpwwe2lem4  10594  fpwwe2lem7  10597  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  fpwwecbv  10604  fpwwelem  10605  canthwelem  10610  canthwe  10611  pwfseqlem4  10622  prdsval  17486  imasval  17543  imasaddfnlem  17560  comfffval  17732  comfeq  17740  oppcval  17747  sscfn1  17852  sscfn2  17853  isssc  17855  ssceq  17861  reschomf  17866  isfunc  17899  idfuval  17911  funcres  17931  funcpropd  17937  fucval  17996  fucpropd  18015  homafval  18064  setcval  18112  catcval  18135  estrcval  18158  estrchomfeqhom  18170  hofval  18286  hofpropd  18301  islat  18467  istsr  18617  cnvtsr  18622  isdir  18632  tsrdir  18638  intopsn  18690  frmdval  18887  resgrpplusfrn  18994  rngcval  20670  rnghmsubcsetclem1  20683  rngccat  20686  ringcval  20699  rhmsubcsetclem1  20712  ringccat  20715  rhmsubcrngclem1  20718  rhmsubcrngc  20720  srhmsubc  20732  rhmsubc  20741  opsrval  22101  matval  22473  ustval  24265  trust  24291  utop2nei  24312  utop3cls  24313  utopreg  24314  ussval  24321  ressuss  24324  tususs  24331  fmucnd  24353  cfilufg  24354  trcfilu  24355  neipcfilu  24357  ispsmet  24366  prdsdsf  24429  prdsxmet  24431  ressprdsds  24433  xpsdsfn2  24440  xpsxmetlem  24441  xpsmet  24444  isxms  24509  isms  24511  xmspropd  24535  mspropd  24536  setsxms  24541  setsms  24542  imasf1oxms  24551  imasf1oms  24552  ressxms  24587  ressms  24588  prdsxmslem2  24591  metuval  24611  nmpropd2  24657  ngppropd  24699  tngngp2  24714  pi1addf  25111  pi1addval  25112  iscms  25409  cmspropd  25413  cmssmscld  25414  cmsss  25415  cssbn  25439  rrxds  25457  rrxmfval  25470  minveclem3a  25491  dvlip2  26059  dchrval  27300  madeval  27927  brcgr  29103  issh  31413  qtophaus  34135  prsssdm  34216  ordtrestNEW  34220  ordtrest2NEW  34222  isrrext  34299  sibfof  34639  satefv  35769  mdvval  35859  msrval  35893  mthmpps  35937  funtransport  36386  fvtransport  36387  prdsbnd2  38299  cnpwstotbnd  38301  isrngo  38401  isrngod  38402  rngosn3  38428  isdivrngo  38454  drngoi  38455  isgrpda  38459  ldualset  39754  aomclem8  43643  intopval  48829  rngcvalALTV  48892  rngchomrnghmresALTV  48906  ringcvalALTV  48916  srhmsubcALTV  48952  nelsubc3lem  49696  0funcg2  49710  imaidfu2  49737  idfullsubc  49787  termcfuncval  50158  cnelsubclem  50229  elpglem3  50339  pgindnf  50342