Theorem sqxpeqd 5693

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   × cxp 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5174  df-xp 5667

This theorem is used by:  xpcoid  6291  hartogslem1  9500  isfin6  10288  fpwwe2cbv  10619  fpwwe2lem2  10621  fpwwe2lem3  10622  fpwwe2lem4  10623  fpwwe2lem7  10626  fpwwe2lem11  10630  fpwwe2lem12  10631  fpwwe2  10632  fpwwecbv  10633  fpwwelem  10634  canthwelem  10639  canthwe  10640  pwfseqlem4  10651  prdsval  17512  imasval  17569  imasaddfnlem  17586  comfffval  17758  comfeq  17766  oppcval  17773  sscfn1  17878  sscfn2  17879  isssc  17881  ssceq  17887  reschomf  17892  isfunc  17925  idfuval  17937  funcres  17957  funcpropd  17963  fucval  18022  fucpropd  18041  homafval  18090  setcval  18138  catcval  18161  estrcval  18184  estrchomfeqhom  18196  hofval  18312  hofpropd  18327  islat  18493  istsr  18643  cnvtsr  18648  isdir  18658  tsrdir  18664  intopsn  18716  frmdval  18914  resgrpplusfrn  19021  rngcval  20726  rnghmsubcsetclem1  20739  rngccat  20742  ringcval  20755  rhmsubcsetclem1  20768  ringccat  20771  rhmsubcrngclem1  20774  rhmsubcrngc  20776  srhmsubc  20788  rhmsubc  20797  opsrval  22206  matval  22577  ustval  24369  trust  24395  utop2nei  24416  utop3cls  24417  utopreg  24418  ussval  24425  ressuss  24428  tususs  24435  fmucnd  24457  cfilufg  24458  trcfilu  24459  neipcfilu  24461  ispsmet  24470  prdsdsf  24533  prdsxmet  24535  ressprdsds  24537  xpsdsfn2  24544  xpsxmetlem  24545  xpsmet  24548  isxms  24613  isms  24615  xmspropd  24639  mspropd  24640  setsxms  24645  setsms  24646  imasf1oxms  24655  imasf1oms  24656  ressxms  24691  ressms  24692  prdsxmslem2  24695  metuval  24715  nmpropd2  24761  ngppropd  24803  tngngp2  24818  pi1addf  25215  pi1addval  25216  iscms  25513  cmspropd  25517  cmssmscld  25518  cmsss  25519  cssbn  25543  rrxds  25561  rrxmfval  25574  minveclem3a  25595  dvlip2  26163  dchrval  27407  madeval  28034  brcgr  29259  issh  31569  qtophaus  34235  prsssdm  34316  ordtrestNEW  34320  ordtrest2NEW  34322  isrrext  34399  sibfof  34739  satefv  35914  mdvval  36004  msrval  36038  mthmpps  36082  funtransport  36531  fvtransport  36532  prdsbnd2  38474  cnpwstotbnd  38476  isrngo  38576  isrngod  38577  rngosn3  38603  isdivrngo  38629  drngoi  38630  isgrpda  38634  ldualset  39927  aomclem8  43816  intopval  48995  rngcvalALTV  49058  rngchomrnghmresALTV  49072  ringcvalALTV  49082  srhmsubcALTV  49118  nelsubc3lem  49876  0funcg2  49890  imaidfu2  49917  idfullsubc  49967  termcfuncval  50338  cnelsubclem  50409  elpglem3  50519  pgindnf  50522