Theorem ineq1i 3949

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

Syntax hints:   = wceq 1628   ∩ cin 3710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-v 3338  df-in 3718

This theorem is referenced by:  in12  3963  inindi  3969  dfrab3  4041  dfif5  4242  disjpr2  4388  disjpr2OLD  4389  disjtpsn  4391  disjtp2  4392  resres  5563  imainrect  5729  predidm  5859  fresaun  6232  fresaunres2  6233  ssenen  8295  hartogslem1  8608  prinfzo0  12697  leiso  13431  f1oun2prg  13858  smumul  15413  setsfun  16091  setsfun0  16092  firest  16291  lsmdisj2r  18294  frgpuplem  18381  ltbwe  19670  tgrest  21161  fiuncmp  21405  ptclsg  21616  metnrmlem3  22861  mbfid  23598  ppi1  25085  cht1  25086  ppiub  25124  chdmj2i  28646  chjassi  28650  pjoml2i  28749  pjoml4i  28751  cmcmlem  28755  mayetes3i  28893  cvmdi  29488  atomli  29546  atabsi  29565  uniin1  29670  disjuniel  29713  imadifxp  29717  gtiso  29783  prsss  30267  ordtrest2NEW  30274  esumnul  30415  measinblem  30588  eulerpartlemt  30738  ballotlem2  30855  ballotlemfp1  30858  ballotlemfval0  30862  chtvalz  31012  mthmpps  31782  dffv5  32333  bj-sscon  33316  bj-discrmoore  33368  mblfinlem2  33756  ismblfin  33759  mbfposadd  33766  itg2addnclem2  33771  asindmre  33804  abeqin  34337  xrnres  34479  diophrw  37820  dnwech  38116  lmhmlnmsplit  38155  rp-fakeuninass  38360  iunrelexp0  38492  nznngen  39013  uzinico2  40288  limsup0  40425  limsupvaluz  40439  sge0sn  41095  31prm  42018