Theorem ineq1d 4117

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 4110	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-rab 3080  df-in 3866

This theorem is referenced by:  iinrab2  4958  disji2  5015  disjprgw  5028  disjprg  5029  disjxun  5031  riinint  5810  fnresdisj  6451  fnimadisj  6464  fninfp  6928  ecinxp  8383  fiint  8829  fival  8910  marypha1lem  8931  kmlem12  9622  fin23lem12  9792  fin23lem30  9803  fin23lem33  9806  ttukeylem1  9970  fpwwe2cbv  10091  fpwwe2lem2  10093  fpwwe2  10104  fzval2  12943  fvinim0ffz  13206  limsupval  14880  limsupgval  14882  ello1  14921  elo1  14932  fsum1p  15157  incexclem  15240  fprod1p  15371  smuval2  15882  smueqlem  15890  smumul  15893  setsdm  16576  isacs2  16983  acsfiel  16984  isacs1i  16987  catcval  17423  resscatc  17432  acsficl  17848  lsmdisj3  18877  lsmdisj3a  18883  dprdres  19219  dprdz  19221  dpjdisj  19244  lspdisj2  19968  indistopon  21702  restopnb  21876  ordtrest2  21905  isnrm  22036  cmpcov  22090  cmpsublem  22100  cmpsub  22101  tgcmp  22102  uncmp  22104  hauscmplem  22107  nconnsubb  22124  isnlly  22170  dissnlocfin  22230  kgeni  22238  kgencn3  22259  ptcld  22314  ptcnplem  22322  alexsublem  22745  alexsubb  22747  alexsubALTlem2  22749  alexsubALTlem4  22751  alexsubALT  22752  tmdgsum2  22797  tsmsval2  22831  ustexsym  22917  metrest  23227  qtopbaslem  23461  cnheibor  23657  bndth  23660  lebnumii  23668  iscph  23872  csscld  23950  clsocv  23951  cphsscph  23952  ovolicc2  24223  voliunlem3  24253  ioombl  24266  uniioombllem2  24284  uniioombllem4  24287  uniioombllem6  24289  mbflimsup  24367  taylfval  25054  chtval  25795  ppival  25812  ppival2  25813  ppival2g  25814  chtfl  25834  ppiprm  25836  chtprm  25838  chtnprm  25839  chtdif  25843  ppidif  25848  prmorcht  25863  chdmj2  29413  cmcmlem  29474  pjoml2  29494  fh2  29502  mdbr  30177  mdi  30178  mdbr3  30180  mdbr4  30181  dmdmd  30183  dmdbr3  30188  dmdbr4  30189  dmdi4  30190  dmdbr5  30191  mddmd2  30192  mdsl1i  30204  cvmdi  30207  mdslmd1lem1  30208  mdslmd1lem2  30209  mdslmd1lem3  30210  mdslmd1lem4  30211  mdslmd1i  30212  mdslmd3i  30215  csmdsymi  30217  mdexchi  30218  atomli  30265  atabsi  30284  sumdmdlem2  30302  dmdbr5ati  30305  difuncomp  30416  disji2f  30439  disjif2  30443  disjxpin  30450  disjunsn  30456  fnresin  30484  cycpmco2f1  30918  cycpmconjslem2  30949  locfinreflem  31312  iscref  31316  ordtrest2NEW  31395  ordtconnlem1  31396  carsgclctunlem1  31804  totprobd  31913  probmeasb  31917  ballotlemfval  31976  ballotlemfp1  31978  ballotlemgun  32011  chtvalz  32129  bnj1385  32333  bnj1326  32527  iccllysconn  32729  satfv1  32842  mvrsval  32984  mrsubvrs  33001  mpstval  33014  msubvrs  33039  nosupbnd2lem1  33484  addsid1  33676  addscllem1  33680  neibastop2lem  34099  neibastop2  34100  neibastop3  34101  limsucncmpi  34184  bj-ismoore  34801  fvineqsnf1  35108  pibt2  35115  ptrest  35337  mblfinlem2  35376  sstotbnd2  35493  cntotbnd  35515  heibor  35540  xrneq1  36070  l1cvat  36632  pmodlem2  37424  pmod2iN  37426  hlmod1i  37433  osumcllem3N  37535  osumcllem9N  37541  pexmidlem6N  37552  pl42lem1N  37556  istrnN  37734  djavalN  38712  dihmeetlem9N  38892  dihmeetlem11N  38894  dihmeetlem12N  38895  dihoml4  38954  djhval  38975  dochexmidlem6  39042  lclkrlem2b  39085  lcfrlem20  39139  lcfrlem23  39142  metakunt20  39667  elrfi  40009  isnacs  40019  mrefg2  40022  mapfzcons2  40034  coeq0i  40068  eldioph2lem2  40076  aomclem8  40379  kelac1  40381  islmodfg  40387  lnr2i  40434  fgraphopab  40528  ntrkbimka  41115  ntrk0kbimka  41116  isotone2  41126  ntrclskb  41146  ntrclsk3  41147  ntrclsk13  41148  neicvgbex  41189  disjrnmpt2  42186  disjinfi  42191  uzinico2  42566  uzinico3  42567  fsumiunss  42584  lptre2pt  42649  limsupresre  42705  limsuplesup  42708  limsupresico  42709  limsupvaluz  42717  limsuplt2  42762  liminfval  42768  limsupge  42770  liminfgval  42771  liminfval2  42777  liminfresico  42780  liminflelimsuplem  42784  liminflelimsup  42785  stoweidlem50  43059  stoweidlem57  43066  subsaliuncllem  43364  sge0val  43372  sge0iunmptlemre  43421  nnfoctbdjlem  43461  iundjiun  43466  vonvolmbllem  43666  smfpimcclem  43805  smfsuplem1  43809  elbigo  45331  isnrm4lem3  45591  aacllem  45721