Theorem sqxpeqd 5663

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-xp 5637

This theorem is referenced by:  xpcoid  6254  hartogslem1  9457  isfin6  10222  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2lem3  10556  fpwwe2lem4  10557  fpwwe2lem7  10560  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  fpwwecbv  10567  fpwwelem  10568  canthwelem  10573  canthwe  10574  pwfseqlem4  10585  prdsval  17418  imasval  17475  imasaddfnlem  17492  comfffval  17664  comfeq  17672  oppcval  17679  sscfn1  17784  sscfn2  17785  isssc  17787  ssceq  17793  reschomf  17798  isfunc  17831  idfuval  17843  funcres  17863  funcpropd  17869  fucval  17928  fucpropd  17947  homafval  17996  setcval  18044  catcval  18067  estrcval  18090  estrchomfeqhom  18102  hofval  18218  hofpropd  18233  islat  18399  istsr  18549  cnvtsr  18554  isdir  18564  tsrdir  18570  intopsn  18622  frmdval  18819  resgrpplusfrn  18926  rngcval  20595  rnghmsubcsetclem1  20608  rngccat  20611  ringcval  20624  rhmsubcsetclem1  20637  ringccat  20640  rhmsubcrngclem1  20643  rhmsubcrngc  20645  srhmsubc  20657  rhmsubc  20666  opsrval  22024  matval  22376  ustval  24168  trust  24194  utop2nei  24215  utop3cls  24216  utopreg  24217  ussval  24224  ressuss  24227  tususs  24234  fmucnd  24256  cfilufg  24257  trcfilu  24258  neipcfilu  24260  ispsmet  24269  prdsdsf  24332  prdsxmet  24334  ressprdsds  24336  xpsdsfn2  24343  xpsxmetlem  24344  xpsmet  24347  isxms  24412  isms  24414  xmspropd  24438  mspropd  24439  setsxms  24444  setsms  24445  imasf1oxms  24454  imasf1oms  24455  ressxms  24490  ressms  24491  prdsxmslem2  24494  metuval  24514  nmpropd2  24560  ngppropd  24602  tngngp2  24617  pi1addf  25014  pi1addval  25015  iscms  25312  cmspropd  25316  cmssmscld  25317  cmsss  25318  cssbn  25342  rrxds  25360  rrxmfval  25373  minveclem3a  25394  dvlip2  25962  dchrval  27197  madeval  27824  brcgr  28969  issh  31279  qtophaus  33980  prsssdm  34061  ordtrestNEW  34065  ordtrest2NEW  34067  isrrext  34144  sibfof  34484  satefv  35596  mdvval  35686  msrval  35720  mthmpps  35764  funtransport  36213  fvtransport  36214  prdsbnd2  38116  cnpwstotbnd  38118  isrngo  38218  isrngod  38219  rngosn3  38245  isdivrngo  38271  drngoi  38272  isgrpda  38276  ldualset  39571  aomclem8  43489  intopval  48678  rngcvalALTV  48741  rngchomrnghmresALTV  48755  ringcvalALTV  48765  srhmsubcALTV  48801  nelsubc3lem  49545  0funcg2  49559  imaidfu2  49586  idfullsubc  49636  termcfuncval  50007  cnelsubclem  50078  elpglem3  50188  pgindnf  50191