Theorem sqxpeqd 5687

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5171  df-xp 5661

This theorem is used by:  xpcoid  6300  hartogslem1  9549  isfin6  10391  fpwwe2cbv  10728  fpwwe2lem2  10730  fpwwe2lem3  10731  fpwwe2lem4  10732  fpwwe2lem7  10735  fpwwe2lem11  10739  fpwwe2lem12  10740  fpwwe2  10741  fpwwecbv  10742  fpwwelem  10743  canthwelem  10748  canthwe  10749  pwfseqlem4  10760  prdsval  17641  imasval  17698  imasaddfnlem  17715  comfffval  17887  comfeq  17895  oppcval  17902  sscfn1  18007  sscfn2  18008  isssc  18010  ssceq  18016  reschomf  18021  isfunc  18054  idfuval  18066  funcres  18086  funcpropd  18092  fucval  18151  fucpropd  18170  homafval  18219  setcval  18267  catcval  18290  estrcval  18313  estrchomfeqhom  18325  hofval  18441  hofpropd  18456  islat  18622  istsr  18772  cnvtsr  18777  isdir  18787  tsrdir  18793  intopsn  18847  frmdval  19062  resgrpplusfrn  19176  rngcval  20885  rnghmsubcsetclem1  20898  rngccat  20901  ringcval  20914  rhmsubcsetclem1  20927  ringccat  20930  rhmsubcrngclem1  20933  rhmsubcrngc  20935  srhmsubc  20947  rhmsubc  20956  opsrval  22370  matval  22741  ustval  24537  trust  24563  utop2nei  24584  utop3cls  24585  utopreg  24586  ussval  24593  ressuss  24596  tususs  24603  fmucnd  24625  cfilufg  24626  trcfilu  24627  neipcfilu  24629  ispsmet  24638  prdsdsf  24701  prdsxmet  24703  ressprdsds  24705  xpsdsfn2  24712  xpsxmetlem  24713  xpsmet  24716  isxms  24781  isms  24783  xmspropd  24807  mspropd  24808  setsxms  24813  setsms  24814  imasf1oxms  24823  imasf1oms  24824  ressxms  24859  ressms  24860  prdsxmslem2  24863  metuval  24883  nmpropd2  24929  ngppropd  24971  tngngp2  24986  pi1addf  25383  pi1addval  25384  iscms  25681  cmspropd  25685  cmssmscld  25686  cmsss  25687  cssbn  25711  rrxds  25729  rrxmfval  25742  minveclem3a  25763  dvlip2  26330  dchrval  27576  madeval  28233  brcgr  29493  issh  31825  qtophaus  34524  prsssdm  34605  ordtrestNEW  34609  ordtrest2NEW  34611  isrrext  34688  sibfof  35028  acwer1prclem  35833  onprcf1acwevdlem1  36002  satefv  36303  mdvval  36393  msrval  36427  mthmpps  36471  funtransport  36929  fvtransport  36930  prdsbnd2  38875  cnpwstotbnd  38877  isrngo  38977  isrngod  38978  rngosn3  39004  isdivrngo  39030  drngoi  39031  isgrpda  39035  ldualset  40328  aomclem8  44209  intopval  49444  rngcvalALTV  49507  rngchomrnghmresALTV  49521  ringcvalALTV  49531  srhmsubcALTV  49567  nelsubc3lem  50329  0funcg2  50344  imaidfu2  50372  idfullsubc  50422  termcfuncval  50812  cnelsubcw  50886  elpglem3  51026  pgindnf  51029