Theorem ineq1i 4207

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

Syntax hints:   = wceq 1539   ∩ cin 3946

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-in 3954

This theorem is referenced by:  in12  4219  inindi  4225  dfrab3  4308  dfif5  4543  disjpr2  4716  disjtpsn  4718  disjtp2  4719  resres  5993  imainrect  6179  predidm  6326  fresaun  6761  fresaunres2  6762  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  25384  ppi1  26904  cht1  26905  ppiub  26943  lrrecse  27664  lrrecpred  27666  chdmj2i  31002  chjassi  31006  pjoml2i  31105  pjoml4i  31107  cmcmlem  31111  mayetes3i  31249  cvmdi  31844  atomli  31902  atabsi  31921  uniin1  32050  disjuniel  32095  imadifxp  32099  gtiso  32189  preiman0  32198  prsss  33194  ordtrest2NEW  33201  esumnul  33344  measinblem  33516  eulerpartlemt  33668  ballotlem2  33785  ballotlemfp1  33788  ballotlemfval0  33792  chtvalz  33939  fmla0disjsuc  34687  mthmpps  34871  dffv5  35200  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  44573  limsup0  44708  limsupvaluz  44722  sge0sn  45393  31prm  46563