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

Theorem sqxpeqd 5030
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 5029 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  X.cxp 5002
This theorem is referenced by:  xpcoid  5553  hartogslem1  7988  isfin6  8701  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwe2lem3  9032  fpwwe2lem8  9036  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  fpwwecbv  9043  fpwwelem  9044  canthwelem  9049  canthwe  9050  pwfseqlem4  9061  prdsval  14852  imasval  14908  imasaddfnlem  14925  comfffval  15093  comfeq  15101  oppcval  15108  sscfn1  15186  sscfn2  15187  isssc  15189  ssceq  15195  reschomf  15200  isfunc  15233  idfuval  15245  funcres  15265  funcpropd  15269  fucval  15327  fucpropd  15346  homafval  15356  setcval  15404  catcval  15423  hofval  15521  hofpropd  15536  islat  15677  istsr  15847  cnvtsr  15852  isdir  15862  tsrdir  15868  intopsn  15882  frmdval  16019  opsrval  18139  matval  18913  ustval  20705  trust  20732  utop2nei  20753  utop3cls  20754  utopreg  20755  ussval  20762  ressuss  20766  tususs  20773  fmucnd  20795  cfilufg  20796  trcfilu  20797  neipcfilu  20799  ispsmet  20808  prdsdsf  20870  prdsxmet  20872  ressprdsds  20874  xpsdsfn2  20881  xpsxmetlem  20882  xpsmet  20885  isxms  20950  isms  20952  xmspropd  20976  mspropd  20977  setsxms  20982  setsms  20983  imasf1oxms  20992  imasf1oms  20993  ressxms  21028  ressms  21029  prdsxmslem2  21032  metuval  21053  nmpropd2  21115  ngppropd  21151  tngngp2  21166  pi1addf  21547  pi1addval  21548  iscms  21784  cmspropd  21788  cmsss  21789  rrxds  21825  rrxmfval  21833  minveclem3a  21842  dvlip2  22396  dchrval  23509  brcgr  24203  isgrp2d  25237  isgrpda  25299  efghgrpOLD  25375  isrngo  25380  isrngod  25381  drngoi  25409  rngosn3  25428  isdivrngo  25433  issh  26125  qtophaus  27839  prsssdm  27899  ordtrestNEW  27903  ordtrest2NEW  27905  isrrext  27981  sibfof  28282  mdvval  28864  msrval  28898  mthmpps  28942  funtransport  29681  fvtransport  29682  prdsbnd2  30291  cnpwstotbnd  30293  aomclem8  31007  intopval  32526  estrcval  32630  estrchomfeqhom  32642  rngcvalOLD  32769  rngcval  32770  rnghmsubcsetclem1  32783  rngccat  32786  rngchomrnghmresOLD  32804  ringcvalOLD  32815  ringcval  32816  rhmsubcsetclem1  32829  ringccat  32832  rhmsubcrngclem1  32835  rhmsubcrngc  32837  srhmsubc  32884  rhmsubc  32898  srhmsubcOLD  32903  bj-diagval  34605  ldualset  34850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator