Theorem ineq1i 4224

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

Syntax hints:   = wceq 1537   ∩ cin 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-in 3970

This theorem is referenced by:  in12  4237  inindi  4243  dfrab3  4325  dfif5  4547  disjpr2  4718  disjtpsn  4720  disjtp2  4721  resres  6013  imainrect  6203  predidm  6349  fresaun  6780  fresaunres2  6781  ssenen  9190  hartogslem1  9580  prinfzo0  13735  leiso  14495  f1oun2prg  14953  smumul  16527  setsfun  17205  setsfun0  17206  firest  17479  lsmdisj2r  19718  frgpuplem  19805  ltbwe  22080  tgrest  23183  fiuncmp  23428  ptclsg  23639  metnrmlem3  24897  mbfid  25684  ppi1  27222  cht1  27223  ppiub  27263  lrrecse  27990  lrrecpred  27992  chdmj2i  31511  chjassi  31515  pjoml2i  31614  pjoml4i  31616  cmcmlem  31620  mayetes3i  31758  cvmdi  32353  atomli  32411  atabsi  32430  uniin1  32572  disjuniel  32617  imadifxp  32621  gtiso  32716  preiman0  32725  nn0disj01  32825  prsss  33877  ordtrest2NEW  33884  esumnul  34029  measinblem  34201  eulerpartlemt  34353  ballotlem2  34470  ballotlemfp1  34473  ballotlemfval0  34477  chtvalz  34623  fmla0disjsuc  35383  mthmpps  35567  dffv5  35906  bj-sscon  37012  bj-discrmoore  37094  mblfinlem2  37645  ismblfin  37648  mbfposadd  37654  itg2addnclem2  37659  asindmre  37690  abeqin  38234  xrnres  38384  redundeq1  38611  refrelsredund4  38614  diophrw  42747  dnwech  43037  lmhmlnmsplit  43076  rp-fakeuninass  43506  iunrelexp0  43692  nznngen  44312  uzinico2  45515  limsup0  45650  limsupvaluz  45664  sge0sn  46335  31prm  47522