Theorem sqxpeqd 5686

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

Syntax hints:   → wi 4   = wceq 1540   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-xp 5660

This theorem is referenced by:  xpcoid  6279  hartogslem1  9556  isfin6  10314  fpwwe2cbv  10644  fpwwe2lem2  10646  fpwwe2lem3  10647  fpwwe2lem4  10648  fpwwe2lem7  10651  fpwwe2lem11  10655  fpwwe2lem12  10656  fpwwe2  10657  fpwwecbv  10658  fpwwelem  10659  canthwelem  10664  canthwe  10665  pwfseqlem4  10676  prdsval  17469  imasval  17525  imasaddfnlem  17542  comfffval  17710  comfeq  17718  oppcval  17725  sscfn1  17830  sscfn2  17831  isssc  17833  ssceq  17839  reschomf  17844  isfunc  17877  idfuval  17889  funcres  17909  funcpropd  17915  fucval  17974  fucpropd  17993  homafval  18042  setcval  18090  catcval  18113  estrcval  18136  estrchomfeqhom  18148  hofval  18264  hofpropd  18279  islat  18443  istsr  18593  cnvtsr  18598  isdir  18608  tsrdir  18614  intopsn  18632  frmdval  18829  resgrpplusfrn  18933  rngcval  20578  rnghmsubcsetclem1  20591  rngccat  20594  ringcval  20607  rhmsubcsetclem1  20620  ringccat  20623  rhmsubcrngclem1  20626  rhmsubcrngc  20628  srhmsubc  20640  rhmsubc  20649  opsrval  22004  matval  22349  ustval  24141  trust  24168  utop2nei  24189  utop3cls  24190  utopreg  24191  ussval  24198  ressuss  24201  tususs  24208  fmucnd  24230  cfilufg  24231  trcfilu  24232  neipcfilu  24234  ispsmet  24243  prdsdsf  24306  prdsxmet  24308  ressprdsds  24310  xpsdsfn2  24317  xpsxmetlem  24318  xpsmet  24321  isxms  24386  isms  24388  xmspropd  24412  mspropd  24413  setsxms  24418  setsms  24419  imasf1oxms  24428  imasf1oms  24429  ressxms  24464  ressms  24465  prdsxmslem2  24468  metuval  24488  nmpropd2  24534  ngppropd  24576  tngngp2  24591  pi1addf  24998  pi1addval  24999  iscms  25297  cmspropd  25301  cmssmscld  25302  cmsss  25303  cssbn  25327  rrxds  25345  rrxmfval  25358  minveclem3a  25379  dvlip2  25952  dchrval  27197  madeval  27812  brcgr  28879  issh  31189  qtophaus  33867  prsssdm  33948  ordtrestNEW  33952  ordtrest2NEW  33954  isrrext  34031  sibfof  34372  satefv  35436  mdvval  35526  msrval  35560  mthmpps  35604  funtransport  36049  fvtransport  36050  prdsbnd2  37819  cnpwstotbnd  37821  isrngo  37921  isrngod  37922  rngosn3  37948  isdivrngo  37974  drngoi  37975  isgrpda  37979  ldualset  39143  aomclem8  43085  intopval  48177  rngcvalALTV  48240  rngchomrnghmresALTV  48254  ringcvalALTV  48264  srhmsubcALTV  48300  nelsubc3lem  49037  0funcg2  49049  imaidfu2  49070  idfullsubc  49100  termcfuncval  49417  cnelsubclem  49480  elpglem3  49577  pgindnf  49580