Theorem ineq1i 4167

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

Syntax hints:   = wceq 1540   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-in 3910

This theorem is referenced by:  in12  4180  inindi  4186  dfrab3  4270  dfif5  4493  disjpr2  4665  disjtpsn  4667  disjtp2  4668  resres  5943  imainrect  6130  predidm  6274  fresaun  6695  fresaunres2  6696  ssenen  9068  hartogslem1  9434  prinfzo0  13601  leiso  14366  f1oun2prg  14824  smumul  16404  setsfun  17082  setsfun0  17083  firest  17336  lsmdisj2r  19564  frgpuplem  19651  ltbwe  21949  tgrest  23044  fiuncmp  23289  ptclsg  23500  metnrmlem3  24748  mbfid  25534  ppi1  27072  cht1  27073  ppiub  27113  lrrecse  27854  lrrecpred  27856  chdmj2i  31426  chjassi  31430  pjoml2i  31529  pjoml4i  31531  cmcmlem  31535  mayetes3i  31673  cvmdi  32268  atomli  32326  atabsi  32345  uniin1  32495  disjuniel  32541  imadifxp  32545  gtiso  32643  preiman0  32652  nn0disj01  32763  prsss  33883  ordtrest2NEW  33890  esumnul  34015  measinblem  34187  eulerpartlemt  34339  ballotlem2  34457  ballotlemfp1  34460  ballotlemfval0  34464  chtvalz  34597  fmla0disjsuc  35371  mthmpps  35555  dffv5  35898  bj-sscon  37003  bj-discrmoore  37085  mblfinlem2  37638  ismblfin  37641  mbfposadd  37647  itg2addnclem2  37652  asindmre  37683  abeqin  38227  xrnres  38374  redundeq1  38606  refrelsredund4  38609  diophrw  42732  dnwech  43021  lmhmlnmsplit  43060  rp-fakeuninass  43489  iunrelexp0  43675  nznngen  44289  uzinico2  45542  limsup0  45675  limsupvaluz  45689  sge0sn  46360  31prm  47581