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

Theorem ineq1i 4189
Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
Hypothesis
Ref Expression
ineq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
ineq1i (𝐴𝐶) = (𝐵𝐶)

Proof of Theorem ineq1i
StepHypRef Expression
1 ineq1i.1 . 2 𝐴 = 𝐵
2 ineq1 4185 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  cin 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-rab 3152  df-in 3947
This theorem is referenced by:  in12  4201  inindi  4207  dfrab3  4282  dfif5  4486  disjpr2  4648  disjtpsn  4650  disjtp2  4651  resres  5865  imainrect  6037  predidm  6169  fresaun  6548  fresaunres2  6549  ssenen  8685  hartogslem1  9000  prinfzo0  13071  leiso  13812  f1oun2prg  14274  smumul  15837  setsfun  16513  setsfun0  16514  firest  16701  lsmdisj2r  18747  frgpuplem  18834  ltbwe  20188  tgrest  21702  fiuncmp  21947  ptclsg  22158  metnrmlem3  23403  mbfid  24170  ppi1  25674  cht1  25675  ppiub  25713  chdmj2i  29192  chjassi  29196  pjoml2i  29295  pjoml4i  29297  cmcmlem  29301  mayetes3i  29439  cvmdi  30034  atomli  30092  atabsi  30111  uniin1  30236  disjuniel  30281  imadifxp  30285  gtiso  30368  prsss  31064  ordtrest2NEW  31071  esumnul  31212  measinblem  31384  eulerpartlemt  31534  ballotlem2  31651  ballotlemfp1  31654  ballotlemfval0  31658  chtvalz  31805  fmla0disjsuc  32548  mthmpps  32732  dffv5  33288  bj-sscon  34244  bj-discrmoore  34303  mblfinlem2  34816  ismblfin  34819  mbfposadd  34825  itg2addnclem2  34830  asindmre  34863  abeqin  35401  xrnres  35536  redundeq1  35750  refrelsredund4  35753  diophrw  39240  dnwech  39532  lmhmlnmsplit  39571  rp-fakeuninass  39766  iunrelexp0  39931  nznngen  40532  uzinico2  41722  limsup0  41859  limsupvaluz  41873  sge0sn  42546  31prm  43611
  Copyright terms: Public domain W3C validator