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 1570   × cxp 5653

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-xp 5661

This theorem is used by:  xpcoid  6288  hartogslem1  9517  isfin6  10305  fpwwe2cbv  10642  fpwwe2lem2  10644  fpwwe2lem3  10645  fpwwe2lem4  10646  fpwwe2lem7  10649  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  fpwwecbv  10656  fpwwelem  10657  canthwelem  10662  canthwe  10663  pwfseqlem4  10674  prdsval  17543  imasval  17600  imasaddfnlem  17617  comfffval  17789  comfeq  17797  oppcval  17804  sscfn1  17909  sscfn2  17910  isssc  17912  ssceq  17918  reschomf  17923  isfunc  17956  idfuval  17968  funcres  17988  funcpropd  17994  fucval  18053  fucpropd  18072  homafval  18121  setcval  18169  catcval  18192  estrcval  18215  estrchomfeqhom  18227  hofval  18343  hofpropd  18358  islat  18524  istsr  18674  cnvtsr  18679  isdir  18689  tsrdir  18695  intopsn  18749  frmdval  18963  resgrpplusfrn  19077  rngcval  20783  rnghmsubcsetclem1  20796  rngccat  20799  ringcval  20812  rhmsubcsetclem1  20825  ringccat  20828  rhmsubcrngclem1  20831  rhmsubcrngc  20833  srhmsubc  20845  rhmsubc  20854  opsrval  22265  matval  22636  ustval  24432  trust  24458  utop2nei  24479  utop3cls  24480  utopreg  24481  ussval  24488  ressuss  24491  tususs  24498  fmucnd  24520  cfilufg  24521  trcfilu  24522  neipcfilu  24524  ispsmet  24533  prdsdsf  24596  prdsxmet  24598  ressprdsds  24600  xpsdsfn2  24607  xpsxmetlem  24608  xpsmet  24611  isxms  24676  isms  24678  xmspropd  24702  mspropd  24703  setsxms  24708  setsms  24709  imasf1oxms  24718  imasf1oms  24719  ressxms  24754  ressms  24755  prdsxmslem2  24758  metuval  24778  nmpropd2  24824  ngppropd  24866  tngngp2  24881  pi1addf  25278  pi1addval  25279  iscms  25576  cmspropd  25580  cmssmscld  25581  cmsss  25582  cssbn  25606  rrxds  25624  rrxmfval  25637  minveclem3a  25658  dvlip2  26225  dchrval  27473  madeval  28100  brcgr  29360  issh  31692  qtophaus  34349  prsssdm  34430  ordtrestNEW  34434  ordtrest2NEW  34436  isrrext  34513  sibfof  34854  satefv  35996  mdvval  36086  msrval  36120  mthmpps  36164  funtransport  36614  fvtransport  36615  prdsbnd2  38548  cnpwstotbnd  38550  isrngo  38650  isrngod  38651  rngosn3  38677  isdivrngo  38703  drngoi  38704  isgrpda  38708  ldualset  40001  aomclem8  43905  intopval  49120  rngcvalALTV  49183  rngchomrnghmresALTV  49197  ringcvalALTV  49207  srhmsubcALTV  49243  nelsubc3lem  49999  0funcg2  50013  imaidfu2  50040  idfullsubc  50090  termcfuncval  50461  cnelsubclem  50532  elpglem3  50642  pgindnf  50645