Theorem ineq1d 4169

Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)

Hypothesis

Ref	Expression
ineq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ineq1d	⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Proof of Theorem ineq1d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ineq1 4163	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   = wceq 1559   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3909

This theorem is referenced by:  iinrab2  5024  disji2  5081  disjprg  5093  disjxun  5095  riinint  5944  fnresdisj  6636  fnimadisj  6648  fninfp  7153  ecinxp  8768  fiint  9265  fival  9352  marypha1lem  9373  kmlem12  10112  fin23lem12  10282  fin23lem30  10293  fin23lem33  10296  ttukeylem1  10460  fpwwe2cbv  10582  fpwwe2lem2  10584  fpwwe2  10595  fzval2  13509  fvinim0ffz  13789  limsupval  15492  limsupgval  15494  ello1  15533  elo1  15544  fsum1p  15771  incexclem  15857  fprod1p  15989  smuval2  16507  smueqlem  16515  smumul  16518  setsdm  17197  isacs2  17676  acsfiel  17677  isacs1i  17680  cat1lem  18120  catcval  18124  resscatc  18133  acsficl  18570  lsmdisj3  19714  lsmdisj3a  19720  dprdres  20061  dprdz  20063  dpjdisj  20086  lspdisj2  21185  indistopon  23049  restopnb  23223  ordtrest2  23252  isnrm  23383  cmpcov  23437  cmpsublem  23447  cmpsub  23448  tgcmp  23449  uncmp  23451  hauscmplem  23454  nconnsubb  23471  isnlly  23517  dissnlocfin  23577  kgeni  23585  kgencn3  23606  ptcld  23661  ptcnplem  23669  alexsublem  24092  alexsubb  24094  alexsubALTlem2  24096  alexsubALTlem4  24098  alexsubALT  24099  tmdgsum2  24144  tsmsval2  24178  ustexsym  24264  metrest  24572  qtopbaslem  24806  cnheibor  25005  bndth  25008  lebnumii  25016  iscph  25220  csscld  25299  clsocv  25300  cphsscph  25301  ovolicc2  25572  voliunlem3  25602  ioombl  25615  uniioombllem2  25633  uniioombllem4  25636  uniioombllem6  25638  mbflimsup  25716  taylfval  26410  chtval  27162  ppival  27179  ppival2  27180  ppival2g  27181  chtfl  27201  ppiprm  27203  chtprm  27205  chtnprm  27206  chtdif  27210  ppidif  27215  prmorcht  27230  nosupbnd2lem1  27767  dfpth2  29886  chdmj2  31690  cmcmlem  31751  pjoml2  31771  fh2  31779  mdbr  32454  mdi  32455  mdbr3  32457  mdbr4  32458  dmdmd  32460  dmdbr3  32465  dmdbr4  32466  dmdi4  32467  dmdbr5  32468  mddmd2  32469  mdsl1i  32481  cvmdi  32484  mdslmd1lem1  32485  mdslmd1lem2  32486  mdslmd1lem3  32487  mdslmd1lem4  32488  mdslmd1i  32489  mdslmd3i  32492  csmdsymi  32494  mdexchi  32495  atomli  32542  atabsi  32561  sumdmdlem2  32579  dmdbr5ati  32582  difuncomp  32713  disji2f  32737  disjif2  32741  disjxpin  32748  disjunsn  32754  fnresin  32787  cycpmco2f1  33265  cycpmconjslem2  33296  locfinreflem  34098  iscref  34102  ordtrest2NEW  34181  ordtconnlem1  34182  carsgclctunlem1  34575  totprobd  34684  probmeasb  34688  ballotlemfval  34748  ballotlemfp1  34750  ballotlemgun  34783  chtvalz  34884  bnj1385  35088  bnj1326  35282  vonf1wev  35412  vonf1owevOLD  35414  iccllysconn  35561  satfv1  35674  mvrsval  35816  mrsubvrs  35833  mpstval  35846  msubvrs  35871  neibastop2lem  36681  neibastop2  36682  neibastop3  36683  limsucncmpi  36766  dfttc4  36851  mh-infprim2bi  36868  bj-ismoore  37556  fvineqsnf1  37865  pibt2  37872  ptrest  38079  mblfinlem2  38118  sstotbnd2  38234  cntotbnd  38256  heibor  38281  xrneq1  38856  disjressuc2  38871  ecqmap  38909  l1cvat  39640  pmodlem2  40432  pmod2iN  40434  hlmod1i  40441  osumcllem3N  40543  osumcllem9N  40549  pexmidlem6N  40560  pl42lem1N  40564  istrnN  40742  djavalN  41720  dihmeetlem9N  41900  dihmeetlem11N  41902  dihmeetlem12N  41903  dihoml4  41962  djhval  41983  dochexmidlem6  42050  lclkrlem2b  42093  lcfrlem20  42147  lcfrlem23  42150  elrfi  43236  isnacs  43246  mrefg2  43249  mapfzcons2  43261  coeq0i  43295  eldioph2lem2  43303  aomclem8  43599  kelac1  43601  islmodfg  43607  lnr2i  43654  fgraphopab  43741  ntrkbimka  44575  ntrk0kbimka  44576  isotone2  44586  ntrclskb  44606  ntrclsk3  44607  ntrclsk13  44608  neicvgbex  44649  disjrnmpt2  45727  disjinfi  45731  uzinico2  46098  uzinico3  46099  fsumiunss  46112  lptre2pt  46175  limsupresre  46231  limsuplesup  46234  limsupresico  46235  limsupvaluz  46243  limsuplt2  46288  liminfval  46294  limsupge  46296  liminfgval  46297  liminfval2  46303  liminfresico  46306  liminflelimsuplem  46310  liminflelimsup  46311  stoweidlem50  46585  stoweidlem57  46592  subsaliuncllem  46892  sge0val  46901  sge0iunmptlemre  46950  nnfoctbdjlem  46990  iundjiun  46995  vonvolmbllem  47195  smfpimcclem  47342  smfsuplem1  47346  f1cof1blem  47629  3f1oss1  47630  grimuhgr  48470  elbigo  49134  restclsseplem  49497  sepnsepo  49506  aacllem  50383