Theorem sqxpeqd 5065

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

Syntax hints:   → wi 4   = wceq 1475   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644  df-xp 5044

This theorem is referenced by:  xpcoid  5593  hartogslem1  8330  isfin6  9005  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwe2lem3  9334  fpwwe2lem8  9338  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  fpwwecbv  9345  fpwwelem  9346  canthwelem  9351  canthwe  9352  pwfseqlem4  9363  prdsval  15938  imasval  15994  imasaddfnlem  16011  comfffval  16181  comfeq  16189  oppcval  16196  sscfn1  16300  sscfn2  16301  isssc  16303  ssceq  16309  reschomf  16314  isfunc  16347  idfuval  16359  funcres  16379  funcpropd  16383  fucval  16441  fucpropd  16460  homafval  16502  setcval  16550  catcval  16569  estrcval  16587  estrchomfeqhom  16599  hofval  16715  hofpropd  16730  islat  16870  istsr  17040  cnvtsr  17045  isdir  17055  tsrdir  17061  intopsn  17076  frmdval  17211  resgrpplusfrn  17259  opsrval  19295  matval  20036  ustval  21816  trust  21843  utop2nei  21864  utop3cls  21865  utopreg  21866  ussval  21873  ressuss  21877  tususs  21884  fmucnd  21906  cfilufg  21907  trcfilu  21908  neipcfilu  21910  ispsmet  21919  prdsdsf  21982  prdsxmet  21984  ressprdsds  21986  xpsdsfn2  21993  xpsxmetlem  21994  xpsmet  21997  isxms  22062  isms  22064  xmspropd  22088  mspropd  22089  setsxms  22094  setsms  22095  imasf1oxms  22104  imasf1oms  22105  ressxms  22140  ressms  22141  prdsxmslem2  22144  metuval  22164  nmpropd2  22209  ngppropd  22251  tngngp2  22266  pi1addf  22655  pi1addval  22656  iscms  22950  cmspropd  22954  cmsss  22955  rrxds  22989  rrxmfval  22997  minveclem3a  23006  dvlip2  23562  dchrval  24759  brcgr  25580  issh  27449  qtophaus  29231  prsssdm  29291  ordtrestNEW  29295  ordtrest2NEW  29297  isrrext  29372  sibfof  29729  mdvval  30655  msrval  30689  mthmpps  30733  funtransport  31308  fvtransport  31309  bj-diagval  32267  prdsbnd2  32764  cnpwstotbnd  32766  isrngo  32866  isrngod  32867  rngosn3  32893  isdivrngo  32919  drngoi  32920  isgrpda  32924  ldualset  33430  aomclem8  36649  intopval  41628  rngcvalALTV  41753  rngcval  41754  rnghmsubcsetclem1  41767  rngccat  41770  rngchomrnghmresALTV  41788  ringcvalALTV  41799  ringcval  41800  rhmsubcsetclem1  41813  ringccat  41816  rhmsubcrngclem1  41819  rhmsubcrngc  41821  srhmsubc  41868  rhmsubc  41882  srhmsubcALTV  41887  elpglem3  42255