Theorem sqxpeqd 5658

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-xp 5632

This theorem is referenced by:  xpcoid  6250  hartogslem1  9452  isfin6  10217  fpwwe2cbv  10548  fpwwe2lem2  10550  fpwwe2lem3  10551  fpwwe2lem4  10552  fpwwe2lem7  10555  fpwwe2lem11  10559  fpwwe2lem12  10560  fpwwe2  10561  fpwwecbv  10562  fpwwelem  10563  canthwelem  10568  canthwe  10569  pwfseqlem4  10580  prdsval  17413  imasval  17470  imasaddfnlem  17487  comfffval  17659  comfeq  17667  oppcval  17674  sscfn1  17779  sscfn2  17780  isssc  17782  ssceq  17788  reschomf  17793  isfunc  17826  idfuval  17838  funcres  17858  funcpropd  17864  fucval  17923  fucpropd  17942  homafval  17991  setcval  18039  catcval  18062  estrcval  18085  estrchomfeqhom  18097  hofval  18213  hofpropd  18228  islat  18394  istsr  18544  cnvtsr  18549  isdir  18559  tsrdir  18565  intopsn  18617  frmdval  18814  resgrpplusfrn  18921  rngcval  20590  rnghmsubcsetclem1  20603  rngccat  20606  ringcval  20619  rhmsubcsetclem1  20632  ringccat  20635  rhmsubcrngclem1  20638  rhmsubcrngc  20640  srhmsubc  20652  rhmsubc  20661  opsrval  22038  matval  22390  ustval  24182  trust  24208  utop2nei  24229  utop3cls  24230  utopreg  24231  ussval  24238  ressuss  24241  tususs  24248  fmucnd  24270  cfilufg  24271  trcfilu  24272  neipcfilu  24274  ispsmet  24283  prdsdsf  24346  prdsxmet  24348  ressprdsds  24350  xpsdsfn2  24357  xpsxmetlem  24358  xpsmet  24361  isxms  24426  isms  24428  xmspropd  24452  mspropd  24453  setsxms  24458  setsms  24459  imasf1oxms  24468  imasf1oms  24469  ressxms  24504  ressms  24505  prdsxmslem2  24508  metuval  24528  nmpropd2  24574  ngppropd  24616  tngngp2  24631  pi1addf  25028  pi1addval  25029  iscms  25326  cmspropd  25330  cmssmscld  25331  cmsss  25332  cssbn  25356  rrxds  25374  rrxmfval  25387  minveclem3a  25408  dvlip2  25976  dchrval  27215  madeval  27842  brcgr  28987  issh  31298  qtophaus  34000  prsssdm  34081  ordtrestNEW  34085  ordtrest2NEW  34087  isrrext  34164  sibfof  34504  satefv  35616  mdvval  35706  msrval  35740  mthmpps  35784  funtransport  36233  fvtransport  36234  prdsbnd2  38134  cnpwstotbnd  38136  isrngo  38236  isrngod  38237  rngosn3  38263  isdivrngo  38289  drngoi  38290  isgrpda  38294  ldualset  39589  aomclem8  43511  intopval  48694  rngcvalALTV  48757  rngchomrnghmresALTV  48771  ringcvalALTV  48781  srhmsubcALTV  48817  nelsubc3lem  49561  0funcg2  49575  imaidfu2  49602  idfullsubc  49652  termcfuncval  50023  cnelsubclem  50094  elpglem3  50204  pgindnf  50207