Theorem sqxpeqd 5657

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

Syntax hints:   → wi 4   = wceq 1542   × cxp 5623

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5162  df-xp 5631

This theorem is referenced by:  xpcoid  6249  hartogslem1  9451  isfin6  10214  fpwwe2cbv  10545  fpwwe2lem2  10547  fpwwe2lem3  10548  fpwwe2lem4  10549  fpwwe2lem7  10552  fpwwe2lem11  10556  fpwwe2lem12  10557  fpwwe2  10558  fpwwecbv  10559  fpwwelem  10560  canthwelem  10565  canthwe  10566  pwfseqlem4  10577  prdsval  17379  imasval  17436  imasaddfnlem  17453  comfffval  17625  comfeq  17633  oppcval  17640  sscfn1  17745  sscfn2  17746  isssc  17748  ssceq  17754  reschomf  17759  isfunc  17792  idfuval  17804  funcres  17824  funcpropd  17830  fucval  17889  fucpropd  17908  homafval  17957  setcval  18005  catcval  18028  estrcval  18051  estrchomfeqhom  18063  hofval  18179  hofpropd  18194  islat  18360  istsr  18510  cnvtsr  18515  isdir  18525  tsrdir  18531  intopsn  18583  frmdval  18780  resgrpplusfrn  18884  rngcval  20555  rnghmsubcsetclem1  20568  rngccat  20571  ringcval  20584  rhmsubcsetclem1  20597  ringccat  20600  rhmsubcrngclem1  20603  rhmsubcrngc  20605  srhmsubc  20617  rhmsubc  20626  opsrval  22005  matval  22359  ustval  24151  trust  24177  utop2nei  24198  utop3cls  24199  utopreg  24200  ussval  24207  ressuss  24210  tususs  24217  fmucnd  24239  cfilufg  24240  trcfilu  24241  neipcfilu  24243  ispsmet  24252  prdsdsf  24315  prdsxmet  24317  ressprdsds  24319  xpsdsfn2  24326  xpsxmetlem  24327  xpsmet  24330  isxms  24395  isms  24397  xmspropd  24421  mspropd  24422  setsxms  24427  setsms  24428  imasf1oxms  24437  imasf1oms  24438  ressxms  24473  ressms  24474  prdsxmslem2  24477  metuval  24497  nmpropd2  24543  ngppropd  24585  tngngp2  24600  pi1addf  25007  pi1addval  25008  iscms  25305  cmspropd  25309  cmssmscld  25310  cmsss  25311  cssbn  25335  rrxds  25353  rrxmfval  25366  minveclem3a  25387  dvlip2  25960  dchrval  27205  madeval  27832  brcgr  28977  issh  31287  qtophaus  33995  prsssdm  34076  ordtrestNEW  34080  ordtrest2NEW  34082  isrrext  34159  sibfof  34499  satefv  35610  mdvval  35700  msrval  35734  mthmpps  35778  funtransport  36227  fvtransport  36228  prdsbnd2  37998  cnpwstotbnd  38000  isrngo  38100  isrngod  38101  rngosn3  38127  isdivrngo  38153  drngoi  38154  isgrpda  38158  ldualset  39453  aomclem8  43370  intopval  48515  rngcvalALTV  48578  rngchomrnghmresALTV  48592  ringcvalALTV  48602  srhmsubcALTV  48638  nelsubc3lem  49382  0funcg2  49396  imaidfu2  49423  idfullsubc  49473  termcfuncval  49844  cnelsubclem  49915  elpglem3  50025  pgindnf  50028