Theorem sqxpeqd 5622

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

Syntax hints:   → wi 4   = wceq 1539   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-opab 5138  df-xp 5596

This theorem is referenced by:  xpcoid  6197  hartogslem1  9310  isfin6  10065  fpwwe2cbv  10395  fpwwe2lem2  10397  fpwwe2lem3  10398  fpwwe2lem7  10402  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  fpwwecbv  10409  fpwwelem  10410  canthwelem  10415  canthwe  10416  pwfseqlem4  10427  prdsval  17175  imasval  17231  imasaddfnlem  17248  comfffval  17416  comfeq  17424  oppcval  17431  sscfn1  17538  sscfn2  17539  isssc  17541  ssceq  17547  reschomf  17553  isfunc  17588  idfuval  17600  funcres  17620  funcpropd  17625  fucval  17684  fucpropd  17704  homafval  17753  setcval  17801  catcval  17824  estrcval  17849  estrchomfeqhom  17861  hofval  17979  hofpropd  17994  islat  18160  istsr  18310  cnvtsr  18315  isdir  18325  tsrdir  18331  intopsn  18347  frmdval  18499  resgrpplusfrn  18602  opsrval  21256  matval  21567  ustval  23363  trust  23390  utop2nei  23411  utop3cls  23412  utopreg  23413  ussval  23420  ressuss  23423  tususs  23431  fmucnd  23453  cfilufg  23454  trcfilu  23455  neipcfilu  23457  ispsmet  23466  prdsdsf  23529  prdsxmet  23531  ressprdsds  23533  xpsdsfn2  23540  xpsxmetlem  23541  xpsmet  23544  isxms  23609  isms  23611  xmspropd  23635  mspropd  23636  setsxms  23643  setsms  23644  imasf1oxms  23654  imasf1oms  23655  ressxms  23690  ressms  23691  prdsxmslem2  23694  metuval  23714  nmpropd2  23760  ngppropd  23802  tngngp2  23825  pi1addf  24219  pi1addval  24220  iscms  24518  cmspropd  24522  cmssmscld  24523  cmsss  24524  cssbn  24548  rrxds  24566  rrxmfval  24579  minveclem3a  24600  dvlip2  25168  dchrval  26391  brcgr  27277  issh  29579  qtophaus  31795  prsssdm  31876  ordtrestNEW  31880  ordtrest2NEW  31882  isrrext  31959  sibfof  32316  satefv  33385  mdvval  33475  msrval  33509  mthmpps  33553  madeval  34045  funtransport  34342  fvtransport  34343  prdsbnd2  35962  cnpwstotbnd  35964  isrngo  36064  isrngod  36065  rngosn3  36091  isdivrngo  36117  drngoi  36118  isgrpda  36122  ldualset  37146  aomclem8  40893  intopval  45407  rngcvalALTV  45530  rngcval  45531  rnghmsubcsetclem1  45544  rngccat  45547  rngchomrnghmresALTV  45565  ringcvalALTV  45576  ringcval  45577  rhmsubcsetclem1  45590  ringccat  45593  rhmsubcrngclem1  45596  rhmsubcrngc  45598  srhmsubc  45645  rhmsubc  45659  srhmsubcALTV  45663  elpglem3  46429