Theorem ineq1i 4169

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

Syntax hints:   = wceq 1570   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3912

This theorem is referenced by:  in12  4181  inindi  4187  dfrab3  4272  dfif5  4504  disjpr2  4679  disjtpsn  4681  disjtp2  4682  uniin1  5039  resres  5991  imainrect  6179  predidm  6327  fresaun  6749  fresaunres2  6750  ssenen  9135  hartogslem1  9500  prinfzo0  13723  leiso  14492  f1oun2prg  14950  smumul  16546  setsfun  17226  setsfun0  17227  firest  17480  lsmdisj2r  19750  frgpuplem  19837  ltbwe  22195  tgrest  23316  fiuncmp  23561  ptclsg  23772  metnrmlem3  25019  mbfid  25794  ppi1  27328  cht1  27329  ppiub  27368  lrrecse  28135  lrrecpred  28137  chdmj2i  31834  chjassi  31838  pjoml2i  31937  pjoml4i  31939  cmcmlem  31943  mayetes3i  32081  cvmdi  32676  atomli  32734  atabsi  32753  disjuniel  32942  imadifxp  32946  gtiso  33046  preiman0  33055  nn0disj01  33163  evlextv  33932  prsss  34306  ordtrest2NEW  34313  esumnul  34438  measinblem  34610  eulerpartlemt  34761  ballotlem2  34879  ballotlemfp1  34882  ballotlemfval0  34886  chtvalz  35016  dfscott3  35512  fmla0disjsuc  35890  mthmpps  36074  dffv5  36414  bj-sscon  37665  bj-discrmoore  37753  mblfinlem2  38309  ismblfin  38312  mbfposadd  38318  itg2addnclem2  38323  asindmre  38354  abeqin  38903  xrnres  39074  redundeq1  39362  refrelsredund4  39365  dfpetparts2  39621  dfpeters2  39623  diophrw  43490  dnwech  43775  lmhmlnmsplit  43814  rp-fakeuninass  44242  iunrelexp0  44428  nznngen  45026  uzinico2  46277  limsup0  46408  limsupvaluz  46422  sge0sn  47093  31prm  48349