Theorem sqxpeqd 5695

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-xp 5669

This theorem is used by:  xpcoid  6295  hartogslem1  9511  isfin6  10299  fpwwe2cbv  10634  fpwwe2lem2  10636  fpwwe2lem3  10637  fpwwe2lem4  10638  fpwwe2lem7  10641  fpwwe2lem11  10645  fpwwe2lem12  10646  fpwwe2  10647  fpwwecbv  10648  fpwwelem  10649  canthwelem  10654  canthwe  10655  pwfseqlem4  10666  prdsval  17534  imasval  17591  imasaddfnlem  17608  comfffval  17780  comfeq  17788  oppcval  17795  sscfn1  17900  sscfn2  17901  isssc  17903  ssceq  17909  reschomf  17914  isfunc  17947  idfuval  17959  funcres  17979  funcpropd  17985  fucval  18044  fucpropd  18063  homafval  18112  setcval  18160  catcval  18183  estrcval  18206  estrchomfeqhom  18218  hofval  18334  hofpropd  18349  islat  18515  istsr  18665  cnvtsr  18670  isdir  18680  tsrdir  18686  intopsn  18740  frmdval  18951  resgrpplusfrn  19065  rngcval  20771  rnghmsubcsetclem1  20784  rngccat  20787  ringcval  20800  rhmsubcsetclem1  20813  ringccat  20816  rhmsubcrngclem1  20819  rhmsubcrngc  20821  srhmsubc  20833  rhmsubc  20842  opsrval  22251  matval  22622  ustval  24415  trust  24441  utop2nei  24462  utop3cls  24463  utopreg  24464  ussval  24471  ressuss  24474  tususs  24481  fmucnd  24503  cfilufg  24504  trcfilu  24505  neipcfilu  24507  ispsmet  24516  prdsdsf  24579  prdsxmet  24581  ressprdsds  24583  xpsdsfn2  24590  xpsxmetlem  24591  xpsmet  24594  isxms  24659  isms  24661  xmspropd  24685  mspropd  24686  setsxms  24691  setsms  24692  imasf1oxms  24701  imasf1oms  24702  ressxms  24737  ressms  24738  prdsxmslem2  24741  metuval  24761  nmpropd2  24807  ngppropd  24849  tngngp2  24864  pi1addf  25261  pi1addval  25262  iscms  25559  cmspropd  25563  cmssmscld  25564  cmsss  25565  cssbn  25589  rrxds  25607  rrxmfval  25620  minveclem3a  25641  dvlip2  26209  dchrval  27453  madeval  28080  brcgr  29309  issh  31635  qtophaus  34294  prsssdm  34375  ordtrestNEW  34379  ordtrest2NEW  34381  isrrext  34458  sibfof  34799  satefv  35947  mdvval  36037  msrval  36071  mthmpps  36115  funtransport  36564  fvtransport  36565  prdsbnd2  38508  cnpwstotbnd  38510  isrngo  38610  isrngod  38611  rngosn3  38637  isdivrngo  38663  drngoi  38664  isgrpda  38668  ldualset  39961  aomclem8  43865  intopval  49043  rngcvalALTV  49106  rngchomrnghmresALTV  49120  ringcvalALTV  49130  srhmsubcALTV  49166  nelsubc3lem  49924  0funcg2  49938  imaidfu2  49965  idfullsubc  50015  termcfuncval  50386  cnelsubclem  50457  elpglem3  50567  pgindnf  50570