Theorem sqxpeqd 5557

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

Syntax hints:   → wi 4   = wceq 1542   × cxp 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-opab 5093  df-xp 5531

This theorem is referenced by:  xpcoid  6122  hartogslem1  9079  isfin6  9800  fpwwe2cbv  10130  fpwwe2lem2  10132  fpwwe2lem3  10133  fpwwe2lem7  10137  fpwwe2lem11  10141  fpwwe2lem12  10142  fpwwe2  10143  fpwwecbv  10144  fpwwelem  10145  canthwelem  10150  canthwe  10151  pwfseqlem4  10162  prdsval  16831  imasval  16887  imasaddfnlem  16904  comfffval  17072  comfeq  17080  oppcval  17087  sscfn1  17192  sscfn2  17193  isssc  17195  ssceq  17201  reschomf  17206  isfunc  17239  idfuval  17251  funcres  17271  funcpropd  17275  fucval  17333  fucpropd  17352  homafval  17401  setcval  17449  catcval  17472  estrcval  17490  estrchomfeqhom  17502  hofval  17618  hofpropd  17633  islat  17773  istsr  17943  cnvtsr  17948  isdir  17958  tsrdir  17964  intopsn  17980  frmdval  18132  resgrpplusfrn  18235  opsrval  20857  matval  21162  ustval  22954  trust  22981  utop2nei  23002  utop3cls  23003  utopreg  23004  ussval  23011  ressuss  23015  tususs  23022  fmucnd  23044  cfilufg  23045  trcfilu  23046  neipcfilu  23048  ispsmet  23057  prdsdsf  23120  prdsxmet  23122  ressprdsds  23124  xpsdsfn2  23131  xpsxmetlem  23132  xpsmet  23135  isxms  23200  isms  23202  xmspropd  23226  mspropd  23227  setsxms  23232  setsms  23233  imasf1oxms  23242  imasf1oms  23243  ressxms  23278  ressms  23279  prdsxmslem2  23282  metuval  23302  nmpropd2  23348  ngppropd  23390  tngngp2  23405  pi1addf  23799  pi1addval  23800  iscms  24097  cmspropd  24101  cmssmscld  24102  cmsss  24103  cssbn  24127  rrxds  24145  rrxmfval  24158  minveclem3a  24179  dvlip2  24747  dchrval  25970  brcgr  26846  issh  29143  qtophaus  31358  prsssdm  31439  ordtrestNEW  31443  ordtrest2NEW  31445  isrrext  31520  sibfof  31877  satefv  32947  mdvval  33037  msrval  33071  mthmpps  33115  madeval  33677  funtransport  33971  fvtransport  33972  prdsbnd2  35576  cnpwstotbnd  35578  isrngo  35678  isrngod  35679  rngosn3  35705  isdivrngo  35731  drngoi  35732  isgrpda  35736  ldualset  36762  aomclem8  40458  intopval  44930  rngcvalALTV  45053  rngcval  45054  rnghmsubcsetclem1  45067  rngccat  45070  rngchomrnghmresALTV  45088  ringcvalALTV  45099  ringcval  45100  rhmsubcsetclem1  45113  ringccat  45116  rhmsubcrngclem1  45119  rhmsubcrngc  45121  srhmsubc  45168  rhmsubc  45182  srhmsubcALTV  45186  elpglem3  45871