Theorem sqxpeqd 5683

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  xpcoid  6293  hartogslem1  9536  isfin6  10378  fpwwe2cbv  10715  fpwwe2lem2  10717  fpwwe2lem3  10718  fpwwe2lem4  10719  fpwwe2lem7  10722  fpwwe2lem11  10726  fpwwe2lem12  10727  fpwwe2  10728  fpwwecbv  10729  fpwwelem  10730  canthwelem  10735  canthwe  10736  pwfseqlem4  10747  prdsval  17626  imasval  17683  imasaddfnlem  17700  comfffval  17872  comfeq  17880  oppcval  17887  sscfn1  17992  sscfn2  17993  isssc  17995  ssceq  18001  reschomf  18006  isfunc  18039  idfuval  18051  funcres  18071  funcpropd  18077  fucval  18136  fucpropd  18155  homafval  18204  setcval  18252  catcval  18275  estrcval  18298  estrchomfeqhom  18310  hofval  18426  hofpropd  18441  islat  18607  istsr  18757  cnvtsr  18762  isdir  18772  tsrdir  18778  intopsn  18832  frmdval  19047  resgrpplusfrn  19161  rngcval  20870  rnghmsubcsetclem1  20883  rngccat  20886  ringcval  20899  rhmsubcsetclem1  20912  ringccat  20915  rhmsubcrngclem1  20918  rhmsubcrngc  20920  srhmsubc  20932  rhmsubc  20941  opsrval  22355  matval  22726  ustval  24522  trust  24548  utop2nei  24569  utop3cls  24570  utopreg  24571  ussval  24578  ressuss  24581  tususs  24588  fmucnd  24610  cfilufg  24611  trcfilu  24612  neipcfilu  24614  ispsmet  24623  prdsdsf  24686  prdsxmet  24688  ressprdsds  24690  xpsdsfn2  24697  xpsxmetlem  24698  xpsmet  24701  isxms  24766  isms  24768  xmspropd  24792  mspropd  24793  setsxms  24798  setsms  24799  imasf1oxms  24808  imasf1oms  24809  ressxms  24844  ressms  24845  prdsxmslem2  24848  metuval  24868  nmpropd2  24914  ngppropd  24956  tngngp2  24971  pi1addf  25368  pi1addval  25369  iscms  25666  cmspropd  25670  cmssmscld  25671  cmsss  25672  cssbn  25696  rrxds  25714  rrxmfval  25727  minveclem3a  25748  dvlip2  26315  dchrval  27561  madeval  28218  brcgr  29478  issh  31810  qtophaus  34468  prsssdm  34549  ordtrestNEW  34553  ordtrest2NEW  34555  isrrext  34632  sibfof  34972  acwer1prclem  35759  onprcf1acwevdlem1  35895  satefv  36179  mdvval  36269  msrval  36303  mthmpps  36347  funtransport  36796  fvtransport  36797  prdsbnd2  38729  cnpwstotbnd  38731  isrngo  38831  isrngod  38832  rngosn3  38858  isdivrngo  38884  drngoi  38885  isgrpda  38889  ldualset  40182  aomclem8  44062  intopval  49298  rngcvalALTV  49361  rngchomrnghmresALTV  49375  ringcvalALTV  49385  srhmsubcALTV  49421  nelsubc3lem  50177  0funcg2  50191  imaidfu2  50218  idfullsubc  50268  termcfuncval  50639  cnelsubclem  50710  elpglem3  50805  pgindnf  50808