Theorem ineq1d 4165

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906

This theorem is used by:  iinrab2  5028  disji2  5087  disjprg  5099  disjxun  5101  riinint  5954  fnresdisj  6657  fnimadisj  6669  fninfp  7177  ecinxp  8806  fiint  9311  fival  9397  marypha1lem  9418  kmlem12  10233  fin23lem12  10402  fin23lem30  10413  fin23lem33  10416  ttukeylem1  10580  fpwwe2cbv  10708  fpwwe2lem2  10710  fpwwe2  10721  fzval2  13635  fvinim0ffz  13917  limsupval  15634  limsupgval  15636  ello1  15675  elo1  15686  fsum1p  15912  incexclem  15998  fprod1p  16128  smuval2  16645  smueqlem  16653  smumul  16656  setsdm  17341  isacs2  17820  acsfiel  17821  isacs1i  17824  cat1lem  18264  catcval  18268  resscatc  18277  acsficl  18714  lsmdisj3  19890  lsmdisj3a  19896  dprdres  20237  dprdz  20239  dpjdisj  20262  lspdisj2  21398  indistopon  23312  restopnb  23486  ordtrest2  23515  isnrm  23646  cmpcov  23700  cmpsublem  23710  cmpsub  23711  tgcmp  23712  uncmp  23714  hauscmplem  23717  nconnsubb  23734  isnlly  23781  dissnlocfin  23841  kgeni  23849  kgencn3  23870  ptcld  23925  ptcnplem  23933  alexsublem  24356  alexsubb  24358  alexsubALTlem2  24360  alexsubALTlem4  24362  alexsubALT  24363  tmdgsum2  24408  tsmsval2  24442  ustexsym  24528  metrest  24836  qtopbaslem  25070  cnheibor  25269  bndth  25272  lebnumii  25280  iscph  25484  csscld  25563  clsocv  25564  cphsscph  25565  ovolicc2  25836  voliunlem3  25866  ioombl  25879  uniioombllem2  25897  uniioombllem4  25900  uniioombllem6  25902  mbflimsup  25980  taylfval  26679  chtval  27430  ppival  27447  ppival2  27448  ppival2g  27449  chtfl  27469  ppiprm  27471  chtprm  27473  chtnprm  27474  chtdif  27478  ppidif  27483  prmorcht  27498  nosupbnd2lem1  28065  dfprlng3  29419  dfpth2  30307  chdmj2  32125  cmcmlem  32186  pjoml2  32206  fh2  32214  mdbr  32889  mdi  32890  mdbr3  32892  mdbr4  32893  dmdmd  32895  dmdbr3  32900  dmdbr4  32901  dmdi4  32902  dmdbr5  32903  mddmd2  32904  mdsl1i  32916  cvmdi  32919  mdslmd1lem1  32920  mdslmd1lem2  32921  mdslmd1lem3  32922  mdslmd1lem4  32923  mdslmd1i  32924  mdslmd3i  32927  csmdsymi  32929  mdexchi  32930  atomli  32977  atabsi  32996  sumdmdlem2  33014  dmdbr5ati  33017  difuncomp  33141  disji2f  33164  disjif2  33168  disjxpin  33175  disjunsn  33181  fnresin  33211  cycpmco2f1  33678  cycpmconjslem2  33709  locfinreflem  34465  iscref  34469  ordtrest2NEW  34548  ordtconnlem1  34549  carsgclctunlem1  34942  totprobd  35051  probmeasb  35055  ballotlemfval  35115  ballotlemfp1  35117  ballotlemgun  35150  chtvalz  35251  bnj1385  35455  bnj1326  35649  vonf1wev  35870  vonf1owevOLD  35872  iccllysconn  35994  satfv1  36107  mvrsval  36249  mrsubvrs  36266  mpstval  36279  msubvrs  36304  neibastop2lem  37128  neibastop2  37129  neibastop3  37130  limsucncmpi  37213  dfttc4  37298  mh-infprim2bi  37315  bj-ismoore  38006  fvineqsnf1  38313  pibt2  38320  ptrest  38517  mblfinlem2  38556  sstotbnd2  38688  cntotbnd  38710  heibor  38735  xrneq1  39308  disjressuc2  39323  ecqmap  39361  l1cvat  40092  pmodlem2  40884  pmod2iN  40886  hlmod1i  40893  osumcllem3N  40995  osumcllem9N  41001  pexmidlem6N  41012  pl42lem1N  41016  istrnN  41194  djavalN  42172  dihmeetlem9N  42352  dihmeetlem11N  42354  dihmeetlem12N  42355  dihoml4  42414  djhval  42435  dochexmidlem6  42502  lclkrlem2b  42545  lcfrlem20  42599  lcfrlem23  42602  elrfi  43684  isnacs  43694  mrefg2  43697  mapfzcons2  43709  coeq0i  43743  eldioph2lem2  43751  aomclem8  44047  kelac1  44049  islmodfg  44055  lnr2i  44102  fgraphopab  44189  ntrkbimka  45023  ntrk0kbimka  45024  isotone2  45034  ntrclskb  45054  ntrclsk3  45055  ntrclsk13  45056  neicvgbex  45097  disjrnmpt2  46172  disjinfi  46176  uzinico2  46542  uzinico3  46543  fsumiunss  46556  lptre2pt  46619  limsupresre  46675  limsuplesup  46678  limsupresico  46679  limsupvaluz  46687  limsuplt2  46732  liminfval  46738  limsupge  46740  liminfgval  46741  liminfval2  46747  liminfresico  46750  liminflelimsuplem  46754  liminflelimsup  46755  stoweidlem50  47029  stoweidlem57  47036  subsaliuncllem  47336  sge0val  47345  sge0iunmptlemre  47394  nnfoctbdjlem  47434  iundjiun  47439  vonvolmbllem  47639  smfpimcclem  47786  smfsuplem1  47790  f1cof1blem  48113  3f1oss1  48114  grimuhgr  48954  elbigo  49632  restclsseplem  49992  sepnsepo  50001  aacllem  50908