Theorem sqxpeqd 5298

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

Syntax hints:   → wi 4   = wceq 1632   × cxp 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-opab 4865  df-xp 5272

This theorem is referenced by:  xpcoid  5837  hartogslem1  8612  isfin6  9314  fpwwe2cbv  9644  fpwwe2lem2  9646  fpwwe2lem3  9647  fpwwe2lem8  9651  fpwwe2lem12  9655  fpwwe2lem13  9656  fpwwe2  9657  fpwwecbv  9658  fpwwelem  9659  canthwelem  9664  canthwe  9665  pwfseqlem4  9676  prdsval  16317  imasval  16373  imasaddfnlem  16390  comfffval  16559  comfeq  16567  oppcval  16574  sscfn1  16678  sscfn2  16679  isssc  16681  ssceq  16687  reschomf  16692  isfunc  16725  idfuval  16737  funcres  16757  funcpropd  16761  fucval  16819  fucpropd  16838  homafval  16880  setcval  16928  catcval  16947  estrcval  16965  estrchomfeqhom  16977  hofval  17093  hofpropd  17108  islat  17248  istsr  17418  cnvtsr  17423  isdir  17433  tsrdir  17439  intopsn  17454  frmdval  17589  resgrpplusfrn  17637  opsrval  19676  matval  20419  ustval  22207  trust  22234  utop2nei  22255  utop3cls  22256  utopreg  22257  ussval  22264  ressuss  22268  tususs  22275  fmucnd  22297  cfilufg  22298  trcfilu  22299  neipcfilu  22301  ispsmet  22310  prdsdsf  22373  prdsxmet  22375  ressprdsds  22377  xpsdsfn2  22384  xpsxmetlem  22385  xpsmet  22388  isxms  22453  isms  22455  xmspropd  22479  mspropd  22480  setsxms  22485  setsms  22486  imasf1oxms  22495  imasf1oms  22496  ressxms  22531  ressms  22532  prdsxmslem2  22535  metuval  22555  nmpropd2  22600  ngppropd  22642  tngngp2  22657  pi1addf  23047  pi1addval  23048  iscms  23342  cmspropd  23346  cmsss  23347  rrxds  23381  rrxmfval  23389  minveclem3a  23398  dvlip2  23957  dchrval  25158  brcgr  25979  issh  28374  qtophaus  30212  prsssdm  30272  ordtrestNEW  30276  ordtrest2NEW  30278  isrrext  30353  sibfof  30711  mdvval  31708  msrval  31742  mthmpps  31786  madeval  32241  funtransport  32444  fvtransport  32445  bj-diagval  33401  prdsbnd2  33907  cnpwstotbnd  33909  isrngo  34009  isrngod  34010  rngosn3  34036  isdivrngo  34062  drngoi  34063  isgrpda  34067  ldualset  34915  aomclem8  38133  intopval  42348  rngcvalALTV  42471  rngcval  42472  rnghmsubcsetclem1  42485  rngccat  42488  rngchomrnghmresALTV  42506  ringcvalALTV  42517  ringcval  42518  rhmsubcsetclem1  42531  ringccat  42534  rhmsubcrngclem1  42537  rhmsubcrngc  42539  srhmsubc  42586  rhmsubc  42600  srhmsubcALTV  42604  elpglem3  42969