Theorem ineq1i 4157

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

Syntax hints:   = wceq 1542   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897

This theorem is referenced by:  in12  4170  inindi  4176  dfrab3  4260  dfif5  4484  disjpr2  4658  disjtpsn  4660  disjtp2  4661  resres  5951  imainrect  6139  predidm  6284  fresaun  6705  fresaunres2  6706  ssenen  9082  hartogslem1  9450  prinfzo0  13644  leiso  14412  f1oun2prg  14870  smumul  16453  setsfun  17132  setsfun0  17133  firest  17386  lsmdisj2r  19651  frgpuplem  19738  ltbwe  22032  tgrest  23134  fiuncmp  23379  ptclsg  23590  metnrmlem3  24837  mbfid  25612  ppi1  27141  cht1  27142  ppiub  27181  lrrecse  27948  lrrecpred  27950  chdmj2i  31568  chjassi  31572  pjoml2i  31671  pjoml4i  31673  cmcmlem  31677  mayetes3i  31815  cvmdi  32410  atomli  32468  atabsi  32487  uniin1  32636  disjuniel  32682  imadifxp  32686  gtiso  32789  preiman0  32798  nn0disj01  32907  evlextv  33701  esplyind  33734  prsss  34076  ordtrest2NEW  34083  esumnul  34208  measinblem  34380  eulerpartlemt  34531  ballotlem2  34649  ballotlemfp1  34652  ballotlemfval0  34656  chtvalz  34789  fmla0disjsuc  35596  mthmpps  35780  dffv5  36120  bj-sscon  37352  bj-discrmoore  37439  mblfinlem2  37993  ismblfin  37996  mbfposadd  38002  itg2addnclem2  38007  asindmre  38038  abeqin  38589  xrnres  38760  redundeq1  39048  refrelsredund4  39051  dfpetparts2  39307  dfpeters2  39309  diophrw  43205  dnwech  43494  lmhmlnmsplit  43533  rp-fakeuninass  43961  iunrelexp0  44147  nznngen  44761  uzinico2  46009  limsup0  46140  limsupvaluz  46154  sge0sn  46825  31prm  48072