Theorem sqxpeqd 5646

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

Syntax hints:   → wi 4   = wceq 1541   × cxp 5612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5152  df-xp 5620

This theorem is referenced by:  xpcoid  6237  hartogslem1  9428  isfin6  10191  fpwwe2cbv  10521  fpwwe2lem2  10523  fpwwe2lem3  10524  fpwwe2lem4  10525  fpwwe2lem7  10528  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  fpwwecbv  10535  fpwwelem  10536  canthwelem  10541  canthwe  10542  pwfseqlem4  10553  prdsval  17359  imasval  17415  imasaddfnlem  17432  comfffval  17604  comfeq  17612  oppcval  17619  sscfn1  17724  sscfn2  17725  isssc  17727  ssceq  17733  reschomf  17738  isfunc  17771  idfuval  17783  funcres  17803  funcpropd  17809  fucval  17868  fucpropd  17887  homafval  17936  setcval  17984  catcval  18007  estrcval  18030  estrchomfeqhom  18042  hofval  18158  hofpropd  18173  islat  18339  istsr  18489  cnvtsr  18494  isdir  18504  tsrdir  18510  intopsn  18562  frmdval  18759  resgrpplusfrn  18863  rngcval  20533  rnghmsubcsetclem1  20546  rngccat  20549  ringcval  20562  rhmsubcsetclem1  20575  ringccat  20578  rhmsubcrngclem1  20581  rhmsubcrngc  20583  srhmsubc  20595  rhmsubc  20604  opsrval  21981  matval  22326  ustval  24118  trust  24144  utop2nei  24165  utop3cls  24166  utopreg  24167  ussval  24174  ressuss  24177  tususs  24184  fmucnd  24206  cfilufg  24207  trcfilu  24208  neipcfilu  24210  ispsmet  24219  prdsdsf  24282  prdsxmet  24284  ressprdsds  24286  xpsdsfn2  24293  xpsxmetlem  24294  xpsmet  24297  isxms  24362  isms  24364  xmspropd  24388  mspropd  24389  setsxms  24394  setsms  24395  imasf1oxms  24404  imasf1oms  24405  ressxms  24440  ressms  24441  prdsxmslem2  24444  metuval  24464  nmpropd2  24510  ngppropd  24552  tngngp2  24567  pi1addf  24974  pi1addval  24975  iscms  25272  cmspropd  25276  cmssmscld  25277  cmsss  25278  cssbn  25302  rrxds  25320  rrxmfval  25333  minveclem3a  25354  dvlip2  25927  dchrval  27172  madeval  27793  brcgr  28878  issh  31188  qtophaus  33849  prsssdm  33930  ordtrestNEW  33934  ordtrest2NEW  33936  isrrext  34013  sibfof  34353  satefv  35458  mdvval  35548  msrval  35582  mthmpps  35626  funtransport  36075  fvtransport  36076  prdsbnd2  37834  cnpwstotbnd  37836  isrngo  37936  isrngod  37937  rngosn3  37963  isdivrngo  37989  drngoi  37990  isgrpda  37994  ldualset  39223  aomclem8  43153  intopval  48301  rngcvalALTV  48364  rngchomrnghmresALTV  48378  ringcvalALTV  48388  srhmsubcALTV  48424  nelsubc3lem  49170  0funcg2  49184  imaidfu2  49211  idfullsubc  49261  termcfuncval  49632  cnelsubclem  49703  elpglem3  49813  pgindnf  49816