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

Theorem ineq1i 3790
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 3787 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  cin 3555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3563
This theorem is referenced by:  in12  3804  inindi  3810  dfrab3  3880  dfif5  4076  disjpr2  4220  disjpr2OLD  4221  disjtpsn  4223  disjtp2  4224  resres  5370  imainrect  5536  predidm  5663  fresaun  6034  fresaunres2  6035  ssenen  8081  hartogslem1  8394  prinfzo0  12450  leiso  13184  f1oun2prg  13601  smumul  15142  setsfun  15817  setsfun0  15818  firest  16017  lsmdisj2r  18022  frgpuplem  18109  ltbwe  19394  tgrest  20876  fiuncmp  21120  ptclsg  21331  metnrmlem3  22577  mbfid  23316  ppi1  24797  cht1  24798  ppiub  24836  chdmj2i  28202  chjassi  28206  pjoml2i  28305  pjoml4i  28307  cmcmlem  28311  mayetes3i  28449  cvmdi  29044  atomli  29102  atabsi  29121  uniin1  29225  disjuniel  29267  imadifxp  29271  gtiso  29333  prsss  29756  ordtrest2NEW  29763  esumnul  29903  measinblem  30076  eulerpartlemt  30226  ballotlem2  30343  ballotlemfp1  30346  ballotlemfval0  30350  mthmpps  31208  dffv5  31694  bj-sscon  32682  mblfinlem2  33100  ismblfin  33103  mbfposadd  33110  itg2addnclem2  33115  asindmre  33148  diophrw  36823  dnwech  37119  lmhmlnmsplit  37158  rp-fakeuninass  37364  iunrelexp0  37496  nznngen  38018  uzinico2  39218  limsup0  39348  limsupvaluz  39362  sge0sn  39919  31prm  40827
  Copyright terms: Public domain W3C validator