Theorem ineq1i 4139

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 4136	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)

Syntax hints:   = wceq 1539   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  in12  4151  inindi  4157  dfrab3  4240  dfif5  4472  disjpr2  4646  disjtpsn  4648  disjtp2  4649  resres  5893  imainrect  6073  predidm  6218  fresaun  6629  fresaunres2  6630  ssenen  8887  hartogslem1  9231  prinfzo0  13354  leiso  14101  f1oun2prg  14558  smumul  16128  setsfun  16800  setsfun0  16801  firest  17060  lsmdisj2r  19206  frgpuplem  19293  ltbwe  21155  tgrest  22218  fiuncmp  22463  ptclsg  22674  metnrmlem3  23930  mbfid  24704  ppi1  26218  cht1  26219  ppiub  26257  chdmj2i  29745  chjassi  29749  pjoml2i  29848  pjoml4i  29850  cmcmlem  29854  mayetes3i  29992  cvmdi  30587  atomli  30645  atabsi  30664  uniin1  30792  disjuniel  30837  imadifxp  30841  gtiso  30935  preiman0  30944  prsss  31768  ordtrest2NEW  31775  esumnul  31916  measinblem  32088  eulerpartlemt  32238  ballotlem2  32355  ballotlemfp1  32358  ballotlemfval0  32362  chtvalz  32509  fmla0disjsuc  33260  mthmpps  33444  lrrecse  34026  lrrecpred  34028  dffv5  34153  bj-sscon  35146  bj-discrmoore  35209  mblfinlem2  35742  ismblfin  35745  mbfposadd  35751  itg2addnclem2  35756  asindmre  35787  abeqin  36319  xrnres  36455  redundeq1  36669  refrelsredund4  36672  diophrw  40497  dnwech  40789  lmhmlnmsplit  40828  rp-fakeuninass  41021  iunrelexp0  41199  nznngen  41823  uzinico2  42990  limsup0  43125  limsupvaluz  43139  sge0sn  43807  31prm  44937