Theorem sqxpeqd 5581

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

Syntax hints:   → wi 4   = wceq 1533   × cxp 5547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-opab 5121  df-xp 5555

This theorem is referenced by:  xpcoid  6135  hartogslem1  9000  isfin6  9716  fpwwe2cbv  10046  fpwwe2lem2  10048  fpwwe2lem3  10049  fpwwe2lem8  10053  fpwwe2lem12  10057  fpwwe2lem13  10058  fpwwe2  10059  fpwwecbv  10060  fpwwelem  10061  canthwelem  10066  canthwe  10067  pwfseqlem4  10078  prdsval  16722  imasval  16778  imasaddfnlem  16795  comfffval  16962  comfeq  16970  oppcval  16977  sscfn1  17081  sscfn2  17082  isssc  17084  ssceq  17090  reschomf  17095  isfunc  17128  idfuval  17140  funcres  17160  funcpropd  17164  fucval  17222  fucpropd  17241  homafval  17283  setcval  17331  catcval  17350  estrcval  17368  estrchomfeqhom  17380  hofval  17496  hofpropd  17511  islat  17651  istsr  17821  cnvtsr  17826  isdir  17836  tsrdir  17842  intopsn  17858  frmdval  18010  resgrpplusfrn  18111  opsrval  20249  matval  21014  ustval  22805  trust  22832  utop2nei  22853  utop3cls  22854  utopreg  22855  ussval  22862  ressuss  22866  tususs  22873  fmucnd  22895  cfilufg  22896  trcfilu  22897  neipcfilu  22899  ispsmet  22908  prdsdsf  22971  prdsxmet  22973  ressprdsds  22975  xpsdsfn2  22982  xpsxmetlem  22983  xpsmet  22986  isxms  23051  isms  23053  xmspropd  23077  mspropd  23078  setsxms  23083  setsms  23084  imasf1oxms  23093  imasf1oms  23094  ressxms  23129  ressms  23130  prdsxmslem2  23133  metuval  23153  nmpropd2  23198  ngppropd  23240  tngngp2  23255  pi1addf  23645  pi1addval  23646  iscms  23942  cmspropd  23946  cmssmscld  23947  cmsss  23948  cssbn  23972  rrxds  23990  rrxmfval  24003  minveclem3a  24024  dvlip2  24586  dchrval  25804  brcgr  26680  issh  28979  qtophaus  31095  prsssdm  31155  ordtrestNEW  31159  ordtrest2NEW  31161  isrrext  31236  sibfof  31593  satefv  32656  mdvval  32746  msrval  32780  mthmpps  32824  madeval  33284  funtransport  33487  fvtransport  33488  prdsbnd2  35067  cnpwstotbnd  35069  isrngo  35169  isrngod  35170  rngosn3  35196  isdivrngo  35222  drngoi  35223  isgrpda  35227  ldualset  36255  aomclem8  39654  intopval  44103  rngcvalALTV  44226  rngcval  44227  rnghmsubcsetclem1  44240  rngccat  44243  rngchomrnghmresALTV  44261  ringcvalALTV  44272  ringcval  44273  rhmsubcsetclem1  44286  ringccat  44289  rhmsubcrngclem1  44292  rhmsubcrngc  44294  srhmsubc  44341  rhmsubc  44355  srhmsubcALTV  44359  elpglem3  44809