Theorem ineq1i 4177

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

Syntax hints:   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  in12  4189  inindi  4195  dfrab3  4280  dfif5  4509  disjpr2  4684  disjtpsn  4686  disjtp2  4687  uniin1  5043  resres  5992  imainrect  6180  predidm  6328  fresaun  6750  fresaunres2  6751  ssenen  9138  hartogslem1  9503  prinfzo0  13726  leiso  14495  f1oun2prg  14953  smumul  16550  setsfun  17230  setsfun0  17231  firest  17484  lsmdisj2r  19754  frgpuplem  19841  ltbwe  22163  tgrest  23284  fiuncmp  23529  ptclsg  23740  metnrmlem3  24987  mbfid  25762  ppi1  27293  cht1  27294  ppiub  27333  lrrecse  28100  lrrecpred  28102  chdmj2i  31774  chjassi  31778  pjoml2i  31877  pjoml4i  31879  cmcmlem  31883  mayetes3i  32021  cvmdi  32616  atomli  32674  atabsi  32693  disjuniel  32882  imadifxp  32886  gtiso  32986  preiman0  32995  nn0disj01  33103  evlextv  33876  prsss  34250  ordtrest2NEW  34257  esumnul  34382  measinblem  34554  eulerpartlemt  34705  ballotlem2  34823  ballotlemfp1  34826  ballotlemfval0  34830  chtvalz  34960  fmla0disjsuc  35788  mthmpps  35972  dffv5  36312  bj-sscon  37552  bj-discrmoore  37640  mblfinlem2  38196  ismblfin  38199  mbfposadd  38205  itg2addnclem2  38210  asindmre  38241  abeqin  38792  xrnres  38963  redundeq1  39251  refrelsredund4  39254  dfpetparts2  39510  dfpeters2  39512  diophrw  43381  dnwech  43666  lmhmlnmsplit  43705  rp-fakeuninass  44133  iunrelexp0  44319  nznngen  44917  uzinico2  46168  limsup0  46299  limsupvaluz  46313  sge0sn  46984  31prm  48237