Theorem ineq1i 4216

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

Syntax hints:   = wceq 1540   ∩ cin 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958

This theorem is referenced by:  in12  4229  inindi  4235  dfrab3  4319  dfif5  4542  disjpr2  4713  disjtpsn  4715  disjtp2  4716  resres  6010  imainrect  6201  predidm  6347  fresaun  6779  fresaunres2  6780  ssenen  9191  hartogslem1  9582  prinfzo0  13738  leiso  14498  f1oun2prg  14956  smumul  16530  setsfun  17208  setsfun0  17209  firest  17477  lsmdisj2r  19703  frgpuplem  19790  ltbwe  22062  tgrest  23167  fiuncmp  23412  ptclsg  23623  metnrmlem3  24883  mbfid  25670  ppi1  27207  cht1  27208  ppiub  27248  lrrecse  27975  lrrecpred  27977  chdmj2i  31501  chjassi  31505  pjoml2i  31604  pjoml4i  31606  cmcmlem  31610  mayetes3i  31748  cvmdi  32343  atomli  32401  atabsi  32420  uniin1  32564  disjuniel  32610  imadifxp  32614  gtiso  32710  preiman0  32719  nn0disj01  32820  prsss  33915  ordtrest2NEW  33922  esumnul  34049  measinblem  34221  eulerpartlemt  34373  ballotlem2  34491  ballotlemfp1  34494  ballotlemfval0  34498  chtvalz  34644  fmla0disjsuc  35403  mthmpps  35587  dffv5  35925  bj-sscon  37030  bj-discrmoore  37112  mblfinlem2  37665  ismblfin  37668  mbfposadd  37674  itg2addnclem2  37679  asindmre  37710  abeqin  38253  xrnres  38403  redundeq1  38630  refrelsredund4  38633  diophrw  42770  dnwech  43060  lmhmlnmsplit  43099  rp-fakeuninass  43529  iunrelexp0  43715  nznngen  44335  uzinico2  45575  limsup0  45709  limsupvaluz  45723  sge0sn  46394  31prm  47584