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

Theorem ineq1i 4182
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 4178 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  cin 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rab 3144  df-in 3940
This theorem is referenced by:  in12  4194  inindi  4200  dfrab3  4275  dfif5  4479  disjpr2  4641  disjtpsn  4643  disjtp2  4644  resres  5859  imainrect  6031  predidm  6163  fresaun  6542  fresaunres2  6543  ssenen  8679  hartogslem1  8994  prinfzo0  13064  leiso  13805  f1oun2prg  14267  smumul  15830  setsfun  16506  setsfun0  16507  firest  16694  lsmdisj2r  18740  frgpuplem  18827  ltbwe  20181  tgrest  21695  fiuncmp  21940  ptclsg  22151  metnrmlem3  23396  mbfid  24163  ppi1  25668  cht1  25669  ppiub  25707  chdmj2i  29186  chjassi  29190  pjoml2i  29289  pjoml4i  29291  cmcmlem  29295  mayetes3i  29433  cvmdi  30028  atomli  30086  atabsi  30105  uniin1  30230  disjuniel  30275  imadifxp  30279  gtiso  30362  prsss  31058  ordtrest2NEW  31065  esumnul  31206  measinblem  31378  eulerpartlemt  31528  ballotlem2  31645  ballotlemfp1  31648  ballotlemfval0  31652  chtvalz  31799  fmla0disjsuc  32542  mthmpps  32726  dffv5  33282  bj-sscon  34238  bj-discrmoore  34297  mblfinlem2  34811  ismblfin  34814  mbfposadd  34820  itg2addnclem2  34825  asindmre  34858  abeqin  35395  xrnres  35530  redundeq1  35744  refrelsredund4  35747  diophrw  39234  dnwech  39526  lmhmlnmsplit  39565  rp-fakeuninass  39760  iunrelexp0  39925  nznngen  40525  uzinico2  41714  limsup0  41851  limsupvaluz  41865  sge0sn  42538  31prm  43637
  Copyright terms: Public domain W3C validator