Theorem sqxpeqd 5694

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

Syntax hints:   → wi 4   = wceq 1567   × cxp 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5178  df-xp 5668

This theorem is referenced by:  xpcoid  6292  hartogslem1  9504  isfin6  10284  fpwwe2cbv  10615  fpwwe2lem2  10617  fpwwe2lem3  10618  fpwwe2lem4  10619  fpwwe2lem7  10622  fpwwe2lem11  10626  fpwwe2lem12  10627  fpwwe2  10628  fpwwecbv  10629  fpwwelem  10630  canthwelem  10635  canthwe  10636  pwfseqlem4  10647  prdsval  17508  imasval  17565  imasaddfnlem  17582  comfffval  17754  comfeq  17762  oppcval  17769  sscfn1  17874  sscfn2  17875  isssc  17877  ssceq  17883  reschomf  17888  isfunc  17921  idfuval  17933  funcres  17953  funcpropd  17959  fucval  18018  fucpropd  18037  homafval  18086  setcval  18134  catcval  18157  estrcval  18180  estrchomfeqhom  18192  hofval  18308  hofpropd  18323  islat  18489  istsr  18639  cnvtsr  18644  isdir  18654  tsrdir  18660  intopsn  18712  frmdval  18910  resgrpplusfrn  19017  rngcval  20703  rnghmsubcsetclem1  20716  rngccat  20719  ringcval  20732  rhmsubcsetclem1  20745  ringccat  20748  rhmsubcrngclem1  20751  rhmsubcrngc  20753  srhmsubc  20765  rhmsubc  20774  opsrval  22166  matval  22537  ustval  24329  trust  24355  utop2nei  24376  utop3cls  24377  utopreg  24378  ussval  24385  ressuss  24388  tususs  24395  fmucnd  24417  cfilufg  24418  trcfilu  24419  neipcfilu  24421  ispsmet  24430  prdsdsf  24493  prdsxmet  24495  ressprdsds  24497  xpsdsfn2  24504  xpsxmetlem  24505  xpsmet  24508  isxms  24573  isms  24575  xmspropd  24599  mspropd  24600  setsxms  24605  setsms  24606  imasf1oxms  24615  imasf1oms  24616  ressxms  24651  ressms  24652  prdsxmslem2  24655  metuval  24675  nmpropd2  24721  ngppropd  24763  tngngp2  24778  pi1addf  25175  pi1addval  25176  iscms  25473  cmspropd  25477  cmssmscld  25478  cmsss  25479  cssbn  25503  rrxds  25521  rrxmfval  25534  minveclem3a  25555  dvlip2  26123  dchrval  27364  madeval  27991  brcgr  29191  issh  31501  qtophaus  34171  prsssdm  34252  ordtrestNEW  34256  ordtrest2NEW  34258  isrrext  34335  sibfof  34675  satefv  35839  mdvval  35929  msrval  35963  mthmpps  36007  funtransport  36456  fvtransport  36457  prdsbnd2  38368  cnpwstotbnd  38370  isrngo  38470  isrngod  38471  rngosn3  38497  isdivrngo  38523  drngoi  38524  isgrpda  38528  ldualset  39823  aomclem8  43714  intopval  48890  rngcvalALTV  48953  rngchomrnghmresALTV  48967  ringcvalALTV  48977  srhmsubcALTV  49013  nelsubc3lem  49767  0funcg2  49781  imaidfu2  49808  idfullsubc  49858  termcfuncval  50229  cnelsubclem  50300  elpglem3  50410  pgindnf  50413