Theorem sqxpeqd 5670

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-xp 5644

This theorem is referenced by:  xpcoid  6263  hartogslem1  9495  isfin6  10253  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwe2lem3  10586  fpwwe2lem4  10587  fpwwe2lem7  10590  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  fpwwecbv  10597  fpwwelem  10598  canthwelem  10603  canthwe  10604  pwfseqlem4  10615  prdsval  17418  imasval  17474  imasaddfnlem  17491  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  18392  istsr  18542  cnvtsr  18547  isdir  18557  tsrdir  18563  intopsn  18581  frmdval  18778  resgrpplusfrn  18882  rngcval  20527  rnghmsubcsetclem1  20540  rngccat  20543  ringcval  20556  rhmsubcsetclem1  20569  ringccat  20572  rhmsubcrngclem1  20575  rhmsubcrngc  20577  srhmsubc  20589  rhmsubc  20598  opsrval  21953  matval  22298  ustval  24090  trust  24117  utop2nei  24138  utop3cls  24139  utopreg  24140  ussval  24147  ressuss  24150  tususs  24157  fmucnd  24179  cfilufg  24180  trcfilu  24181  neipcfilu  24183  ispsmet  24192  prdsdsf  24255  prdsxmet  24257  ressprdsds  24259  xpsdsfn2  24266  xpsxmetlem  24267  xpsmet  24270  isxms  24335  isms  24337  xmspropd  24361  mspropd  24362  setsxms  24367  setsms  24368  imasf1oxms  24377  imasf1oms  24378  ressxms  24413  ressms  24414  prdsxmslem2  24417  metuval  24437  nmpropd2  24483  ngppropd  24525  tngngp2  24540  pi1addf  24947  pi1addval  24948  iscms  25245  cmspropd  25249  cmssmscld  25250  cmsss  25251  cssbn  25275  rrxds  25293  rrxmfval  25306  minveclem3a  25327  dvlip2  25900  dchrval  27145  madeval  27760  brcgr  28827  issh  31137  qtophaus  33826  prsssdm  33907  ordtrestNEW  33911  ordtrest2NEW  33913  isrrext  33990  sibfof  34331  satefv  35401  mdvval  35491  msrval  35525  mthmpps  35569  funtransport  36019  fvtransport  36020  prdsbnd2  37789  cnpwstotbnd  37791  isrngo  37891  isrngod  37892  rngosn3  37918  isdivrngo  37944  drngoi  37945  isgrpda  37949  ldualset  39118  aomclem8  43050  intopval  48190  rngcvalALTV  48253  rngchomrnghmresALTV  48267  ringcvalALTV  48277  srhmsubcALTV  48313  nelsubc3lem  49059  0funcg2  49073  imaidfu2  49100  idfullsubc  49150  termcfuncval  49521  cnelsubclem  49592  elpglem3  49702  pgindnf  49705