Theorem sqxpeqd 5720

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

Syntax hints:   → wi 4   = wceq 1536   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-xp 5694

This theorem is referenced by:  xpcoid  6311  hartogslem1  9579  isfin6  10337  fpwwe2cbv  10667  fpwwe2lem2  10669  fpwwe2lem3  10670  fpwwe2lem4  10671  fpwwe2lem7  10674  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  fpwwecbv  10681  fpwwelem  10682  canthwelem  10687  canthwe  10688  pwfseqlem4  10699  prdsval  17501  imasval  17557  imasaddfnlem  17574  comfffval  17742  comfeq  17750  oppcval  17757  sscfn1  17864  sscfn2  17865  isssc  17867  ssceq  17873  reschomf  17879  isfunc  17914  idfuval  17926  funcres  17946  funcpropd  17953  fucval  18013  fucpropd  18033  homafval  18082  setcval  18130  catcval  18153  estrcval  18178  estrchomfeqhom  18190  hofval  18308  hofpropd  18323  islat  18490  istsr  18640  cnvtsr  18645  isdir  18655  tsrdir  18661  intopsn  18679  frmdval  18876  resgrpplusfrn  18980  rngcval  20634  rnghmsubcsetclem1  20647  rngccat  20650  ringcval  20663  rhmsubcsetclem1  20676  ringccat  20679  rhmsubcrngclem1  20682  rhmsubcrngc  20684  srhmsubc  20696  rhmsubc  20705  opsrval  22081  matval  22430  ustval  24226  trust  24253  utop2nei  24274  utop3cls  24275  utopreg  24276  ussval  24283  ressuss  24286  tususs  24294  fmucnd  24316  cfilufg  24317  trcfilu  24318  neipcfilu  24320  ispsmet  24329  prdsdsf  24392  prdsxmet  24394  ressprdsds  24396  xpsdsfn2  24403  xpsxmetlem  24404  xpsmet  24407  isxms  24472  isms  24474  xmspropd  24498  mspropd  24499  setsxms  24506  setsms  24507  imasf1oxms  24517  imasf1oms  24518  ressxms  24553  ressms  24554  prdsxmslem2  24557  metuval  24577  nmpropd2  24623  ngppropd  24665  tngngp2  24688  pi1addf  25093  pi1addval  25094  iscms  25392  cmspropd  25396  cmssmscld  25397  cmsss  25398  cssbn  25422  rrxds  25440  rrxmfval  25453  minveclem3a  25474  dvlip2  26048  dchrval  27292  madeval  27905  brcgr  28929  issh  31236  qtophaus  33796  prsssdm  33877  ordtrestNEW  33881  ordtrest2NEW  33883  isrrext  33962  sibfof  34321  satefv  35398  mdvval  35488  msrval  35522  mthmpps  35566  funtransport  36012  fvtransport  36013  prdsbnd2  37781  cnpwstotbnd  37783  isrngo  37883  isrngod  37884  rngosn3  37910  isdivrngo  37936  drngoi  37937  isgrpda  37941  ldualset  39106  aomclem8  43049  intopval  48045  rngcvalALTV  48108  rngchomrnghmresALTV  48122  ringcvalALTV  48132  srhmsubcALTV  48168  elpglem3  48943  pgindnf  48946