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

Theorem inteqd 4667
Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
inteqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
inteqd (𝜑 𝐴 = 𝐵)

Proof of Theorem inteqd
StepHypRef Expression
1 inteqd.1 . 2 (𝜑𝐴 = 𝐵)
2 inteq 4665 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2syl 17 1 (𝜑 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637   cint 4662
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 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781
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 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-int 4663
This theorem is referenced by:  intprg  4696  elreldm  5545  ordintdif  5981  fniinfv  6472  onsucmin  7245  elxp5  7335  1stval2  7409  2ndval2  7410  fundmen  8260  xpsnen  8277  unblem2  8446  unblem3  8447  fiint  8470  elfi2  8553  fi0  8559  elfiun  8569  tcvalg  8855  tz9.12lem3  8893  rankvalb  8901  rankvalg  8921  ranksnb  8931  rankonidlem  8932  cardval3  9055  cardidm  9062  cfval  9348  cflim3  9363  coftr  9374  isfin3ds  9430  fin23lem17  9439  fin23lem39  9451  isf33lem  9467  isf34lem5  9479  isf34lem6  9481  wuncval  9843  tskmval  9940  cleq1  13941  dfrtrcl2  14019  mrcfval  16467  mrcval  16469  cycsubg2  17827  efgval  18325  lspfval  19174  lspval  19176  lsppropd  19219  aspval  19531  aspval2  19550  clsfval  21037  clsval  21049  clsval2  21062  hauscmplem  21417  cmpfi  21419  1stcfb  21456  fclscmp  22041  spanval  28514  chsupid  28593  sigagenval  30522  kur14  31515  mclsval  31777  scutval  32226  igenval  34165  pclfvalN  35663  pclvalN  35664  diaintclN  36833  docaffvalN  36896  docafvalN  36897  docavalN  36898  dibintclN  36942  dihglb2  37117  dihintcl  37119  mzpval  37791  dnnumch3lem  38111  aomclem8  38126  rgspnval  38233  iotain  39111  salgenval  41014
  Copyright terms: Public domain W3C validator