Theorem ineq1i 4135

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

Syntax hints:   = wceq 1538   ∩ cin 3880

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888

This theorem is referenced by:  in12  4147  inindi  4153  dfrab3  4230  dfif5  4441  disjpr2  4609  disjtpsn  4611  disjtp2  4612  resres  5831  imainrect  6005  predidm  6138  fresaun  6523  fresaunres2  6524  ssenen  8675  hartogslem1  8990  prinfzo0  13071  leiso  13813  f1oun2prg  14270  smumul  15832  setsfun  16510  setsfun0  16511  firest  16698  lsmdisj2r  18803  frgpuplem  18890  ltbwe  20712  tgrest  21764  fiuncmp  22009  ptclsg  22220  metnrmlem3  23466  mbfid  24239  ppi1  25749  cht1  25750  ppiub  25788  chdmj2i  29265  chjassi  29269  pjoml2i  29368  pjoml4i  29370  cmcmlem  29374  mayetes3i  29512  cvmdi  30107  atomli  30165  atabsi  30184  uniin1  30315  disjuniel  30360  imadifxp  30364  gtiso  30460  preiman0  30469  prsss  31269  ordtrest2NEW  31276  esumnul  31417  measinblem  31589  eulerpartlemt  31739  ballotlem2  31856  ballotlemfp1  31859  ballotlemfval0  31863  chtvalz  32010  fmla0disjsuc  32758  mthmpps  32942  dffv5  33498  bj-sscon  34465  bj-discrmoore  34526  mblfinlem2  35095  ismblfin  35098  mbfposadd  35104  itg2addnclem2  35109  asindmre  35140  abeqin  35674  xrnres  35810  redundeq1  36024  refrelsredund4  36027  diophrw  39700  dnwech  39992  lmhmlnmsplit  40031  rp-fakeuninass  40224  iunrelexp0  40403  nznngen  41020  uzinico2  42199  limsup0  42336  limsupvaluz  42350  sge0sn  43018  31prm  44114