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

Theorem inteqd 4856
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 4854 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2syl 17 1 (𝜑 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538   cint 4851
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-ral 3135  df-int 4852
This theorem is referenced by:  intprg  4885  elreldm  5782  ordintdif  6218  fniinfv  6724  onsucmin  7521  elxp5  7614  1stval2  7692  2ndval2  7693  fundmen  8570  xpsnen  8588  unblem2  8759  unblem3  8760  fiint  8783  elfi2  8866  fi0  8872  elfiun  8882  tcvalg  9168  tz9.12lem3  9206  rankvalb  9214  rankvalg  9234  ranksnb  9244  rankonidlem  9245  cardval3  9369  cardidm  9376  harsucnn  9415  cfval  9658  cflim3  9673  coftr  9684  isfin3ds  9740  fin23lem17  9749  fin23lem39  9761  isf33lem  9777  isf34lem5  9789  isf34lem6  9791  wuncval  10153  tskmval  10250  cleq1  14334  dfrtrcl2  14412  mrcfval  16870  mrcval  16872  cycsubg2  18344  efgval  18834  lspfval  19736  lspval  19738  lsppropd  19781  aspval  20557  aspval2  20582  clsfval  21628  clsval  21640  clsval2  21653  hauscmplem  22009  cmpfi  22011  1stcfb  22048  fclscmp  22633  spanval  29114  chsupid  29193  intimafv  30454  zarclsint  31194  sigagenval  31473  kur14  32537  mclsval  32884  scutval  33339  igenval  35457  pclfvalN  37143  pclvalN  37144  diaintclN  38312  docaffvalN  38375  docafvalN  38376  docavalN  38377  dibintclN  38421  dihglb2  38596  dihintcl  38598  mzpval  39603  dnnumch3lem  39920  aomclem8  39935  rgspnval  40042  iotain  41055  salgenval  42902
  Copyright terms: Public domain W3C validator