Theorem ineq1i 4237

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

Syntax hints:   = wceq 1537   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  in12  4250  inindi  4256  dfrab3  4338  dfif5  4564  disjpr2  4738  disjtpsn  4740  disjtp2  4741  resres  6022  imainrect  6212  predidm  6358  fresaun  6792  fresaunres2  6793  ssenen  9217  hartogslem1  9611  prinfzo0  13755  leiso  14508  f1oun2prg  14966  smumul  16539  setsfun  17218  setsfun0  17219  firest  17492  lsmdisj2r  19727  frgpuplem  19814  ltbwe  22085  tgrest  23188  fiuncmp  23433  ptclsg  23644  metnrmlem3  24902  mbfid  25689  ppi1  27225  cht1  27226  ppiub  27266  lrrecse  27993  lrrecpred  27995  chdmj2i  31514  chjassi  31518  pjoml2i  31617  pjoml4i  31619  cmcmlem  31623  mayetes3i  31761  cvmdi  32356  atomli  32414  atabsi  32433  uniin1  32574  disjuniel  32619  imadifxp  32623  gtiso  32712  preiman0  32721  nn0disj01  32822  prsss  33862  ordtrest2NEW  33869  esumnul  34012  measinblem  34184  eulerpartlemt  34336  ballotlem2  34453  ballotlemfp1  34456  ballotlemfval0  34460  chtvalz  34606  fmla0disjsuc  35366  mthmpps  35550  dffv5  35888  bj-sscon  36995  bj-discrmoore  37077  mblfinlem2  37618  ismblfin  37621  mbfposadd  37627  itg2addnclem2  37632  asindmre  37663  abeqin  38208  xrnres  38358  redundeq1  38585  refrelsredund4  38588  diophrw  42715  dnwech  43005  lmhmlnmsplit  43044  rp-fakeuninass  43478  iunrelexp0  43664  nznngen  44285  uzinico2  45480  limsup0  45615  limsupvaluz  45629  sge0sn  46300  31prm  47471