Theorem ineq1i 4208

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

Syntax hints:   = wceq 1541   ∩ cin 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3955

This theorem is referenced by:  in12  4220  inindi  4226  dfrab3  4309  dfif5  4544  disjpr2  4717  disjtpsn  4719  disjtp2  4720  resres  5994  imainrect  6180  predidm  6327  fresaun  6762  fresaunres2  6763  ssenen  9153  hartogslem1  9539  prinfzo0  13675  leiso  14424  f1oun2prg  14872  smumul  16438  setsfun  17108  setsfun0  17109  firest  17382  lsmdisj2r  19594  frgpuplem  19681  ltbwe  21818  tgrest  22883  fiuncmp  23128  ptclsg  23339  metnrmlem3  24597  mbfid  25376  ppi1  26892  cht1  26893  ppiub  26931  lrrecse  27652  lrrecpred  27654  chdmj2i  30990  chjassi  30994  pjoml2i  31093  pjoml4i  31095  cmcmlem  31099  mayetes3i  31237  cvmdi  31832  atomli  31890  atabsi  31909  uniin1  32038  disjuniel  32083  imadifxp  32087  gtiso  32177  preiman0  32186  prsss  33182  ordtrest2NEW  33189  esumnul  33332  measinblem  33504  eulerpartlemt  33656  ballotlem2  33773  ballotlemfp1  33776  ballotlemfval0  33780  chtvalz  33927  fmla0disjsuc  34675  mthmpps  34859  dffv5  35188  bj-sscon  36213  bj-discrmoore  36295  mblfinlem2  36829  ismblfin  36832  mbfposadd  36838  itg2addnclem2  36843  asindmre  36874  abeqin  37423  xrnres  37575  redundeq1  37802  refrelsredund4  37805  diophrw  41799  dnwech  42092  lmhmlnmsplit  42131  rp-fakeuninass  42569  iunrelexp0  42755  nznngen  43377  uzinico2  44574  limsup0  44709  limsupvaluz  44723  sge0sn  45394  31prm  46564