Theorem sqxpeqd 5670

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5173  df-xp 5644

This theorem is referenced by:  xpcoid  6247  hartogslem1  9487  isfin6  10245  fpwwe2cbv  10575  fpwwe2lem2  10577  fpwwe2lem3  10578  fpwwe2lem7  10582  fpwwe2lem11  10586  fpwwe2lem12  10587  fpwwe2  10588  fpwwecbv  10589  fpwwelem  10590  canthwelem  10595  canthwe  10596  pwfseqlem4  10607  prdsval  17351  imasval  17407  imasaddfnlem  17424  comfffval  17592  comfeq  17600  oppcval  17607  sscfn1  17714  sscfn2  17715  isssc  17717  ssceq  17723  reschomf  17729  isfunc  17764  idfuval  17776  funcres  17796  funcpropd  17801  fucval  17860  fucpropd  17880  homafval  17929  setcval  17977  catcval  18000  estrcval  18025  estrchomfeqhom  18037  hofval  18155  hofpropd  18170  islat  18336  istsr  18486  cnvtsr  18491  isdir  18501  tsrdir  18507  intopsn  18523  frmdval  18675  resgrpplusfrn  18778  opsrval  21484  matval  21795  ustval  23591  trust  23618  utop2nei  23639  utop3cls  23640  utopreg  23641  ussval  23648  ressuss  23651  tususs  23659  fmucnd  23681  cfilufg  23682  trcfilu  23683  neipcfilu  23685  ispsmet  23694  prdsdsf  23757  prdsxmet  23759  ressprdsds  23761  xpsdsfn2  23768  xpsxmetlem  23769  xpsmet  23772  isxms  23837  isms  23839  xmspropd  23863  mspropd  23864  setsxms  23871  setsms  23872  imasf1oxms  23882  imasf1oms  23883  ressxms  23918  ressms  23919  prdsxmslem2  23922  metuval  23942  nmpropd2  23988  ngppropd  24030  tngngp2  24053  pi1addf  24447  pi1addval  24448  iscms  24746  cmspropd  24750  cmssmscld  24751  cmsss  24752  cssbn  24776  rrxds  24794  rrxmfval  24807  minveclem3a  24828  dvlip2  25396  dchrval  26619  madeval  27225  brcgr  27912  issh  30213  qtophaus  32506  prsssdm  32587  ordtrestNEW  32591  ordtrest2NEW  32593  isrrext  32670  sibfof  33029  satefv  34095  mdvval  34185  msrval  34219  mthmpps  34263  funtransport  34692  fvtransport  34693  prdsbnd2  36327  cnpwstotbnd  36329  isrngo  36429  isrngod  36430  rngosn3  36456  isdivrngo  36482  drngoi  36483  isgrpda  36487  ldualset  37660  aomclem8  41446  intopval  46256  rngcvalALTV  46379  rngcval  46380  rnghmsubcsetclem1  46393  rngccat  46396  rngchomrnghmresALTV  46414  ringcvalALTV  46425  ringcval  46426  rhmsubcsetclem1  46439  ringccat  46442  rhmsubcrngclem1  46445  rhmsubcrngc  46447  srhmsubc  46494  rhmsubc  46508  srhmsubcALTV  46512  elpglem3  47278  pgindnf  47281