MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sqxpeqd Structured version   Visualization version   GIF version

Theorem sqxpeqd 5342
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
StepHypRef Expression
1 xpeq1d.1 . 2 (𝜑𝐴 = 𝐵)
21, 1xpeq12d 5341 1 (𝜑 → (𝐴 × 𝐴) = (𝐵 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637   × cxp 5309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-opab 4907  df-xp 5317
This theorem is referenced by:  xpcoid  5890  hartogslem1  8682  isfin6  9403  fpwwe2cbv  9733  fpwwe2lem2  9735  fpwwe2lem3  9736  fpwwe2lem8  9740  fpwwe2lem12  9744  fpwwe2lem13  9745  fpwwe2  9746  fpwwecbv  9747  fpwwelem  9748  canthwelem  9753  canthwe  9754  pwfseqlem4  9765  prdsval  16316  imasval  16372  imasaddfnlem  16389  comfffval  16558  comfeq  16566  oppcval  16573  sscfn1  16677  sscfn2  16678  isssc  16680  ssceq  16686  reschomf  16691  isfunc  16724  idfuval  16736  funcres  16756  funcpropd  16760  fucval  16818  fucpropd  16837  homafval  16879  setcval  16927  catcval  16946  estrcval  16964  estrchomfeqhom  16976  hofval  17093  hofpropd  17108  islat  17248  istsr  17418  cnvtsr  17423  isdir  17433  tsrdir  17439  intopsn  17454  frmdval  17589  resgrpplusfrn  17637  opsrval  19679  matval  20424  ustval  22216  trust  22243  utop2nei  22264  utop3cls  22265  utopreg  22266  ussval  22273  ressuss  22277  tususs  22284  fmucnd  22306  cfilufg  22307  trcfilu  22308  neipcfilu  22310  ispsmet  22319  prdsdsf  22382  prdsxmet  22384  ressprdsds  22386  xpsdsfn2  22393  xpsxmetlem  22394  xpsmet  22397  isxms  22462  isms  22464  xmspropd  22488  mspropd  22489  setsxms  22494  setsms  22495  imasf1oxms  22504  imasf1oms  22505  ressxms  22540  ressms  22541  prdsxmslem2  22544  metuval  22564  nmpropd2  22609  ngppropd  22651  tngngp2  22666  pi1addf  23056  pi1addval  23057  iscms  23352  cmspropd  23356  cmsss  23357  rrxds  23392  rrxmfval  23400  minveclem3a  23409  dvlip2  23971  dchrval  25172  brcgr  25993  issh  28392  qtophaus  30227  prsssdm  30287  ordtrestNEW  30291  ordtrest2NEW  30293  isrrext  30368  sibfof  30726  mdvval  31722  msrval  31756  mthmpps  31800  madeval  32254  funtransport  32457  fvtransport  32458  bj-diagval  33405  prdsbnd2  33903  cnpwstotbnd  33905  isrngo  34005  isrngod  34006  rngosn3  34032  isdivrngo  34058  drngoi  34059  isgrpda  34063  ldualset  34903  aomclem8  38129  intopval  42403  rngcvalALTV  42526  rngcval  42527  rnghmsubcsetclem1  42540  rngccat  42543  rngchomrnghmresALTV  42561  ringcvalALTV  42572  ringcval  42573  rhmsubcsetclem1  42586  ringccat  42589  rhmsubcrngclem1  42592  rhmsubcrngc  42594  srhmsubc  42641  rhmsubc  42655  srhmsubcALTV  42659  elpglem3  43024
  Copyright terms: Public domain W3C validator