Theorem sqxpeqd 5656

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpcoid  6248  hartogslem1  9447  isfin6  10210  fpwwe2cbv  10541  fpwwe2lem2  10543  fpwwe2lem3  10544  fpwwe2lem4  10545  fpwwe2lem7  10548  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  fpwwecbv  10555  fpwwelem  10556  canthwelem  10561  canthwe  10562  pwfseqlem4  10573  prdsval  17375  imasval  17432  imasaddfnlem  17449  comfffval  17621  comfeq  17629  oppcval  17636  sscfn1  17741  sscfn2  17742  isssc  17744  ssceq  17750  reschomf  17755  isfunc  17788  idfuval  17800  funcres  17820  funcpropd  17826  fucval  17885  fucpropd  17904  homafval  17953  setcval  18001  catcval  18024  estrcval  18047  estrchomfeqhom  18059  hofval  18175  hofpropd  18190  islat  18356  istsr  18506  cnvtsr  18511  isdir  18521  tsrdir  18527  intopsn  18579  frmdval  18776  resgrpplusfrn  18880  rngcval  20551  rnghmsubcsetclem1  20564  rngccat  20567  ringcval  20580  rhmsubcsetclem1  20593  ringccat  20596  rhmsubcrngclem1  20599  rhmsubcrngc  20601  srhmsubc  20613  rhmsubc  20622  opsrval  22001  matval  22355  ustval  24147  trust  24173  utop2nei  24194  utop3cls  24195  utopreg  24196  ussval  24203  ressuss  24206  tususs  24213  fmucnd  24235  cfilufg  24236  trcfilu  24237  neipcfilu  24239  ispsmet  24248  prdsdsf  24311  prdsxmet  24313  ressprdsds  24315  xpsdsfn2  24322  xpsxmetlem  24323  xpsmet  24326  isxms  24391  isms  24393  xmspropd  24417  mspropd  24418  setsxms  24423  setsms  24424  imasf1oxms  24433  imasf1oms  24434  ressxms  24469  ressms  24470  prdsxmslem2  24473  metuval  24493  nmpropd2  24539  ngppropd  24581  tngngp2  24596  pi1addf  25003  pi1addval  25004  iscms  25301  cmspropd  25305  cmssmscld  25306  cmsss  25307  cssbn  25331  rrxds  25349  rrxmfval  25362  minveclem3a  25383  dvlip2  25956  dchrval  27201  madeval  27828  brcgr  28973  issh  31283  qtophaus  33993  prsssdm  34074  ordtrestNEW  34078  ordtrest2NEW  34080  isrrext  34157  sibfof  34497  satefv  35608  mdvval  35698  msrval  35732  mthmpps  35776  funtransport  36225  fvtransport  36226  prdsbnd2  37992  cnpwstotbnd  37994  isrngo  38094  isrngod  38095  rngosn3  38121  isdivrngo  38147  drngoi  38148  isgrpda  38152  ldualset  39381  aomclem8  43299  intopval  48444  rngcvalALTV  48507  rngchomrnghmresALTV  48521  ringcvalALTV  48531  srhmsubcALTV  48567  nelsubc3lem  49311  0funcg2  49325  imaidfu2  49352  idfullsubc  49402  termcfuncval  49773  cnelsubclem  49844  elpglem3  49954  pgindnf  49957