Theorem ineq1i 4173

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

Syntax hints:   = wceq 1541   ∩ cin 3912

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-in 3920

This theorem is referenced by:  in12  4185  inindi  4191  dfrab3  4274  dfif5  4507  disjpr2  4679  disjtpsn  4681  disjtp2  4682  resres  5955  imainrect  6138  predidm  6285  fresaun  6718  fresaunres2  6719  ssenen  9102  hartogslem1  9487  prinfzo0  13621  leiso  14370  f1oun2prg  14818  smumul  16384  setsfun  17054  setsfun0  17055  firest  17328  lsmdisj2r  19481  frgpuplem  19568  ltbwe  21482  tgrest  22547  fiuncmp  22792  ptclsg  23003  metnrmlem3  24261  mbfid  25036  ppi1  26550  cht1  26551  ppiub  26589  lrrecse  27297  lrrecpred  27299  chdmj2i  30487  chjassi  30491  pjoml2i  30590  pjoml4i  30592  cmcmlem  30596  mayetes3i  30734  cvmdi  31329  atomli  31387  atabsi  31406  uniin1  31537  disjuniel  31582  imadifxp  31586  gtiso  31682  preiman0  31691  prsss  32586  ordtrest2NEW  32593  esumnul  32736  measinblem  32908  eulerpartlemt  33060  ballotlem2  33177  ballotlemfp1  33180  ballotlemfval0  33184  chtvalz  33331  fmla0disjsuc  34079  mthmpps  34263  dffv5  34585  bj-sscon  35573  bj-discrmoore  35655  mblfinlem2  36189  ismblfin  36192  mbfposadd  36198  itg2addnclem2  36203  asindmre  36234  abeqin  36785  xrnres  36937  redundeq1  37164  refrelsredund4  37167  diophrw  41140  dnwech  41433  lmhmlnmsplit  41472  rp-fakeuninass  41910  iunrelexp0  42096  nznngen  42718  uzinico2  43920  limsup0  44055  limsupvaluz  44069  sge0sn  44740  31prm  45909