Theorem ineq1i 3961

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

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		ineq1 3958	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)

Syntax hints:   = wceq 1631   ∩ cin 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730

This theorem is referenced by:  in12  3973  inindi  3979  dfrab3  4050  dfif5  4241  disjpr2  4385  disjtpsn  4387  disjtp2  4388  resres  5548  imainrect  5714  predidm  5843  fresaun  6213  fresaunres2  6214  ssenen  8288  hartogslem1  8601  prinfzo0  12708  leiso  13438  f1oun2prg  13864  smumul  15416  setsfun  16093  setsfun0  16094  firest  16294  lsmdisj2r  18298  frgpuplem  18385  ltbwe  19680  tgrest  21177  fiuncmp  21421  ptclsg  21632  metnrmlem3  22877  mbfid  23616  ppi1  25104  cht1  25105  ppiub  25143  chdmj2i  28674  chjassi  28678  pjoml2i  28777  pjoml4i  28779  cmcmlem  28783  mayetes3i  28921  cvmdi  29516  atomli  29574  atabsi  29593  uniin1  29698  disjuniel  29741  imadifxp  29745  gtiso  29811  prsss  30295  ordtrest2NEW  30302  esumnul  30443  measinblem  30616  eulerpartlemt  30766  ballotlem2  30883  ballotlemfp1  30886  ballotlemfval0  30890  chtvalz  31040  mthmpps  31810  dffv5  32361  bj-sscon  33338  bj-discrmoore  33391  mblfinlem2  33773  ismblfin  33776  mbfposadd  33782  itg2addnclem2  33787  asindmre  33820  abeqin  34353  xrnres  34495  diophrw  37841  dnwech  38137  lmhmlnmsplit  38176  rp-fakeuninass  38381  iunrelexp0  38513  nznngen  39034  uzinico2  40300  limsup0  40437  limsupvaluz  40451  sge0sn  41106  31prm  42033