Theorem ineq1i 4156

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

Syntax hints:   = wceq 1542   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  in12  4169  inindi  4175  dfrab3  4259  dfif5  4483  disjpr2  4657  disjtpsn  4659  disjtp2  4660  resres  5957  imainrect  6145  predidm  6290  fresaun  6711  fresaunres2  6712  ssenen  9089  hartogslem1  9457  prinfzo0  13653  leiso  14421  f1oun2prg  14879  smumul  16462  setsfun  17141  setsfun0  17142  firest  17395  lsmdisj2r  19660  frgpuplem  19747  ltbwe  22022  tgrest  23124  fiuncmp  23369  ptclsg  23580  metnrmlem3  24827  mbfid  25602  ppi1  27127  cht1  27128  ppiub  27167  lrrecse  27934  lrrecpred  27936  chdmj2i  31553  chjassi  31557  pjoml2i  31656  pjoml4i  31658  cmcmlem  31662  mayetes3i  31800  cvmdi  32395  atomli  32453  atabsi  32472  uniin1  32621  disjuniel  32667  imadifxp  32671  gtiso  32774  preiman0  32783  nn0disj01  32892  evlextv  33686  esplyind  33719  prsss  34060  ordtrest2NEW  34067  esumnul  34192  measinblem  34364  eulerpartlemt  34515  ballotlem2  34633  ballotlemfp1  34636  ballotlemfval0  34640  chtvalz  34773  fmla0disjsuc  35580  mthmpps  35764  dffv5  36104  bj-sscon  37336  bj-discrmoore  37423  mblfinlem2  37979  ismblfin  37982  mbfposadd  37988  itg2addnclem2  37993  asindmre  38024  abeqin  38575  xrnres  38746  redundeq1  39034  refrelsredund4  39037  dfpetparts2  39293  dfpeters2  39295  diophrw  43191  dnwech  43476  lmhmlnmsplit  43515  rp-fakeuninass  43943  iunrelexp0  44129  nznngen  44743  uzinico2  45991  limsup0  46122  limsupvaluz  46136  sge0sn  46807  31prm  48060