Theorem sqxpeqd 5673

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  xpcoid  6266  hartogslem1  9502  isfin6  10260  fpwwe2cbv  10590  fpwwe2lem2  10592  fpwwe2lem3  10593  fpwwe2lem4  10594  fpwwe2lem7  10597  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  fpwwecbv  10604  fpwwelem  10605  canthwelem  10610  canthwe  10611  pwfseqlem4  10622  prdsval  17425  imasval  17481  imasaddfnlem  17498  comfffval  17666  comfeq  17674  oppcval  17681  sscfn1  17786  sscfn2  17787  isssc  17789  ssceq  17795  reschomf  17800  isfunc  17833  idfuval  17845  funcres  17865  funcpropd  17871  fucval  17930  fucpropd  17949  homafval  17998  setcval  18046  catcval  18069  estrcval  18092  estrchomfeqhom  18104  hofval  18220  hofpropd  18235  islat  18399  istsr  18549  cnvtsr  18554  isdir  18564  tsrdir  18570  intopsn  18588  frmdval  18785  resgrpplusfrn  18889  rngcval  20534  rnghmsubcsetclem1  20547  rngccat  20550  ringcval  20563  rhmsubcsetclem1  20576  ringccat  20579  rhmsubcrngclem1  20582  rhmsubcrngc  20584  srhmsubc  20596  rhmsubc  20605  opsrval  21960  matval  22305  ustval  24097  trust  24124  utop2nei  24145  utop3cls  24146  utopreg  24147  ussval  24154  ressuss  24157  tususs  24164  fmucnd  24186  cfilufg  24187  trcfilu  24188  neipcfilu  24190  ispsmet  24199  prdsdsf  24262  prdsxmet  24264  ressprdsds  24266  xpsdsfn2  24273  xpsxmetlem  24274  xpsmet  24277  isxms  24342  isms  24344  xmspropd  24368  mspropd  24369  setsxms  24374  setsms  24375  imasf1oxms  24384  imasf1oms  24385  ressxms  24420  ressms  24421  prdsxmslem2  24424  metuval  24444  nmpropd2  24490  ngppropd  24532  tngngp2  24547  pi1addf  24954  pi1addval  24955  iscms  25252  cmspropd  25256  cmssmscld  25257  cmsss  25258  cssbn  25282  rrxds  25300  rrxmfval  25313  minveclem3a  25334  dvlip2  25907  dchrval  27152  madeval  27767  brcgr  28834  issh  31144  qtophaus  33833  prsssdm  33914  ordtrestNEW  33918  ordtrest2NEW  33920  isrrext  33997  sibfof  34338  satefv  35408  mdvval  35498  msrval  35532  mthmpps  35576  funtransport  36026  fvtransport  36027  prdsbnd2  37796  cnpwstotbnd  37798  isrngo  37898  isrngod  37899  rngosn3  37925  isdivrngo  37951  drngoi  37952  isgrpda  37956  ldualset  39125  aomclem8  43057  intopval  48194  rngcvalALTV  48257  rngchomrnghmresALTV  48271  ringcvalALTV  48281  srhmsubcALTV  48317  nelsubc3lem  49063  0funcg2  49077  imaidfu2  49104  idfullsubc  49154  termcfuncval  49525  cnelsubclem  49596  elpglem3  49706  pgindnf  49709