Theorem ineq1i 4175

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

Syntax hints:   = wceq 1540   ∩ cin 3910

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 3403  df-in 3918

This theorem is referenced by:  in12  4188  inindi  4194  dfrab3  4278  dfif5  4501  disjpr2  4673  disjtpsn  4675  disjtp2  4676  resres  5952  imainrect  6142  predidm  6287  fresaun  6713  fresaunres2  6714  ssenen  9092  hartogslem1  9471  prinfzo0  13635  leiso  14400  f1oun2prg  14859  smumul  16439  setsfun  17117  setsfun0  17118  firest  17371  lsmdisj2r  19591  frgpuplem  19678  ltbwe  21927  tgrest  23022  fiuncmp  23267  ptclsg  23478  metnrmlem3  24726  mbfid  25512  ppi1  27050  cht1  27051  ppiub  27091  lrrecse  27825  lrrecpred  27827  chdmj2i  31384  chjassi  31388  pjoml2i  31487  pjoml4i  31489  cmcmlem  31493  mayetes3i  31631  cvmdi  32226  atomli  32284  atabsi  32303  uniin1  32453  disjuniel  32499  imadifxp  32503  gtiso  32597  preiman0  32606  nn0disj01  32716  prsss  33879  ordtrest2NEW  33886  esumnul  34011  measinblem  34183  eulerpartlemt  34335  ballotlem2  34453  ballotlemfp1  34456  ballotlemfval0  34460  chtvalz  34593  fmla0disjsuc  35358  mthmpps  35542  dffv5  35885  bj-sscon  36990  bj-discrmoore  37072  mblfinlem2  37625  ismblfin  37628  mbfposadd  37634  itg2addnclem2  37639  asindmre  37670  abeqin  38214  xrnres  38361  redundeq1  38593  refrelsredund4  38596  diophrw  42720  dnwech  43010  lmhmlnmsplit  43049  rp-fakeuninass  43478  iunrelexp0  43664  nznngen  44278  uzinico2  45532  limsup0  45665  limsupvaluz  45679  sge0sn  46350  31prm  47571