Theorem sqxpeqd 5717

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691

This theorem is referenced by:  xpcoid  6310  hartogslem1  9582  isfin6  10340  fpwwe2cbv  10670  fpwwe2lem2  10672  fpwwe2lem3  10673  fpwwe2lem4  10674  fpwwe2lem7  10677  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  fpwwecbv  10684  fpwwelem  10685  canthwelem  10690  canthwe  10691  pwfseqlem4  10702  prdsval  17500  imasval  17556  imasaddfnlem  17573  comfffval  17741  comfeq  17749  oppcval  17756  sscfn1  17861  sscfn2  17862  isssc  17864  ssceq  17870  reschomf  17875  isfunc  17909  idfuval  17921  funcres  17941  funcpropd  17947  fucval  18006  fucpropd  18025  homafval  18074  setcval  18122  catcval  18145  estrcval  18168  estrchomfeqhom  18180  hofval  18297  hofpropd  18312  islat  18478  istsr  18628  cnvtsr  18633  isdir  18643  tsrdir  18649  intopsn  18667  frmdval  18864  resgrpplusfrn  18968  rngcval  20618  rnghmsubcsetclem1  20631  rngccat  20634  ringcval  20647  rhmsubcsetclem1  20660  ringccat  20663  rhmsubcrngclem1  20666  rhmsubcrngc  20668  srhmsubc  20680  rhmsubc  20689  opsrval  22064  matval  22415  ustval  24211  trust  24238  utop2nei  24259  utop3cls  24260  utopreg  24261  ussval  24268  ressuss  24271  tususs  24279  fmucnd  24301  cfilufg  24302  trcfilu  24303  neipcfilu  24305  ispsmet  24314  prdsdsf  24377  prdsxmet  24379  ressprdsds  24381  xpsdsfn2  24388  xpsxmetlem  24389  xpsmet  24392  isxms  24457  isms  24459  xmspropd  24483  mspropd  24484  setsxms  24491  setsms  24492  imasf1oxms  24502  imasf1oms  24503  ressxms  24538  ressms  24539  prdsxmslem2  24542  metuval  24562  nmpropd2  24608  ngppropd  24650  tngngp2  24673  pi1addf  25080  pi1addval  25081  iscms  25379  cmspropd  25383  cmssmscld  25384  cmsss  25385  cssbn  25409  rrxds  25427  rrxmfval  25440  minveclem3a  25461  dvlip2  26034  dchrval  27278  madeval  27891  brcgr  28915  issh  31227  qtophaus  33835  prsssdm  33916  ordtrestNEW  33920  ordtrest2NEW  33922  isrrext  34001  sibfof  34342  satefv  35419  mdvval  35509  msrval  35543  mthmpps  35587  funtransport  36032  fvtransport  36033  prdsbnd2  37802  cnpwstotbnd  37804  isrngo  37904  isrngod  37905  rngosn3  37931  isdivrngo  37957  drngoi  37958  isgrpda  37962  ldualset  39126  aomclem8  43073  intopval  48118  rngcvalALTV  48181  rngchomrnghmresALTV  48195  ringcvalALTV  48205  srhmsubcALTV  48241  0funcg2  48917  elpglem3  49232  pgindnf  49235