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  5949  imainrect  6137  predidm  6282  fresaun  6703  fresaunres2  6704  ssenen  9080  hartogslem1  9448  prinfzo0  13642  leiso  14410  f1oun2prg  14868  smumul  16451  setsfun  17130  setsfun0  17131  firest  17384  lsmdisj2r  19649  frgpuplem  19736  ltbwe  22031  tgrest  23133  fiuncmp  23378  ptclsg  23589  metnrmlem3  24836  mbfid  25611  ppi1  27145  cht1  27146  ppiub  27186  lrrecse  27953  lrrecpred  27955  chdmj2i  31573  chjassi  31577  pjoml2i  31676  pjoml4i  31678  cmcmlem  31682  mayetes3i  31820  cvmdi  32415  atomli  32473  atabsi  32492  uniin1  32641  disjuniel  32687  imadifxp  32691  gtiso  32794  preiman0  32803  nn0disj01  32912  evlextv  33706  esplyind  33739  prsss  34081  ordtrest2NEW  34088  esumnul  34213  measinblem  34385  eulerpartlemt  34536  ballotlem2  34654  ballotlemfp1  34657  ballotlemfval0  34661  chtvalz  34794  fmla0disjsuc  35601  mthmpps  35785  dffv5  36125  bj-sscon  37349  bj-discrmoore  37436  mblfinlem2  37990  ismblfin  37993  mbfposadd  37999  itg2addnclem2  38004  asindmre  38035  abeqin  38586  xrnres  38757  redundeq1  39045  refrelsredund4  39048  dfpetparts2  39304  dfpeters2  39306  diophrw  43202  dnwech  43491  lmhmlnmsplit  43530  rp-fakeuninass  43958  iunrelexp0  44144  nznngen  44758  uzinico2  46006  limsup0  46137  limsupvaluz  46151  sge0sn  46822  31prm  48057