Theorem ineq1i 4196

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

Syntax hints:   = wceq 1540   ∩ cin 3930

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938

This theorem is referenced by:  in12  4209  inindi  4215  dfrab3  4299  dfif5  4522  disjpr2  4694  disjtpsn  4696  disjtp2  4697  resres  5984  imainrect  6175  predidm  6320  fresaun  6754  fresaunres2  6755  ssenen  9170  hartogslem1  9561  prinfzo0  13720  leiso  14482  f1oun2prg  14941  smumul  16517  setsfun  17195  setsfun0  17196  firest  17451  lsmdisj2r  19671  frgpuplem  19758  ltbwe  22007  tgrest  23102  fiuncmp  23347  ptclsg  23558  metnrmlem3  24806  mbfid  25593  ppi1  27131  cht1  27132  ppiub  27172  lrrecse  27906  lrrecpred  27908  chdmj2i  31468  chjassi  31472  pjoml2i  31571  pjoml4i  31573  cmcmlem  31577  mayetes3i  31715  cvmdi  32310  atomli  32368  atabsi  32387  uniin1  32537  disjuniel  32583  imadifxp  32587  gtiso  32683  preiman0  32692  nn0disj01  32802  prsss  33952  ordtrest2NEW  33959  esumnul  34084  measinblem  34256  eulerpartlemt  34408  ballotlem2  34526  ballotlemfp1  34529  ballotlemfval0  34533  chtvalz  34666  fmla0disjsuc  35425  mthmpps  35609  dffv5  35947  bj-sscon  37052  bj-discrmoore  37134  mblfinlem2  37687  ismblfin  37690  mbfposadd  37696  itg2addnclem2  37701  asindmre  37732  abeqin  38275  xrnres  38425  redundeq1  38652  refrelsredund4  38655  diophrw  42749  dnwech  43039  lmhmlnmsplit  43078  rp-fakeuninass  43507  iunrelexp0  43693  nznngen  44307  uzinico2  45557  limsup0  45690  limsupvaluz  45704  sge0sn  46375  31prm  47578