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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  iinrab2  5028  disji2  5087  disjprg  5099  disjxun  5101  riinint  5956  fnresdisj  6652  fnimadisj  6664  fninfp  7172  ecinxp  8792  fiint  9296  fival  9382  marypha1lem  9403  kmlem12  10164  fin23lem12  10333  fin23lem30  10344  fin23lem33  10347  ttukeylem1  10511  fpwwe2cbv  10639  fpwwe2lem2  10641  fpwwe2  10652  fzval2  13564  fvinim0ffz  13845  limsupval  15561  limsupgval  15563  ello1  15602  elo1  15613  fsum1p  15839  incexclem  15925  fprod1p  16055  smuval2  16572  smueqlem  16580  smumul  16583  setsdm  17262  isacs2  17741  acsfiel  17742  isacs1i  17745  cat1lem  18185  catcval  18189  resscatc  18198  acsficl  18635  lsmdisj3  19810  lsmdisj3a  19816  dprdres  20157  dprdz  20159  dpjdisj  20182  lspdisj2  21314  indistopon  23226  restopnb  23400  ordtrest2  23429  isnrm  23560  cmpcov  23614  cmpsublem  23624  cmpsub  23625  tgcmp  23626  uncmp  23628  hauscmplem  23631  nconnsubb  23648  isnlly  23695  dissnlocfin  23755  kgeni  23763  kgencn3  23784  ptcld  23839  ptcnplem  23847  alexsublem  24270  alexsubb  24272  alexsubALTlem2  24274  alexsubALTlem4  24276  alexsubALT  24277  tmdgsum2  24322  tsmsval2  24356  ustexsym  24442  metrest  24750  qtopbaslem  24984  cnheibor  25183  bndth  25186  lebnumii  25194  iscph  25398  csscld  25477  clsocv  25478  cphsscph  25479  ovolicc2  25750  voliunlem3  25780  ioombl  25793  uniioombllem2  25811  uniioombllem4  25814  uniioombllem6  25816  mbflimsup  25894  taylfval  26595  chtval  27346  ppival  27363  ppival2  27364  ppival2g  27365  chtfl  27385  ppiprm  27387  chtprm  27389  chtnprm  27390  chtdif  27394  ppidif  27399  prmorcht  27414  nosupbnd2lem1  27951  dfprlng3  29305  dfpth2  30193  chdmj2  32011  cmcmlem  32072  pjoml2  32092  fh2  32100  mdbr  32775  mdi  32776  mdbr3  32778  mdbr4  32779  dmdmd  32781  dmdbr3  32786  dmdbr4  32787  dmdi4  32788  dmdbr5  32789  mddmd2  32790  mdsl1i  32802  cvmdi  32805  mdslmd1lem1  32806  mdslmd1lem2  32807  mdslmd1lem3  32808  mdslmd1lem4  32809  mdslmd1i  32810  mdslmd3i  32813  csmdsymi  32815  mdexchi  32816  atomli  32863  atabsi  32882  sumdmdlem2  32900  dmdbr5ati  32903  difuncomp  33027  disji2f  33050  disjif2  33054  disjxpin  33061  disjunsn  33067  fnresin  33097  cycpmco2f1  33564  cycpmconjslem2  33595  locfinreflem  34350  iscref  34354  ordtrest2NEW  34433  ordtconnlem1  34434  carsgclctunlem1  34828  totprobd  34937  probmeasb  34941  ballotlemfval  35001  ballotlemfp1  35003  ballotlemgun  35036  chtvalz  35137  bnj1385  35341  bnj1326  35535  vonf1wev  35705  vonf1owevOLD  35707  iccllysconn  35829  satfv1  35942  mvrsval  36084  mrsubvrs  36101  mpstval  36114  msubvrs  36139  neibastop2lem  36979  neibastop2  36980  neibastop3  36981  limsucncmpi  37064  dfttc4  37149  mh-infprim2bi  37166  bj-ismoore  37855  fvineqsnf1  38164  pibt2  38171  ptrest  38368  mblfinlem2  38407  sstotbnd2  38524  cntotbnd  38546  heibor  38571  xrneq1  39144  disjressuc2  39159  ecqmap  39197  l1cvat  39928  pmodlem2  40720  pmod2iN  40722  hlmod1i  40729  osumcllem3N  40831  osumcllem9N  40837  pexmidlem6N  40848  pl42lem1N  40852  istrnN  41030  djavalN  42008  dihmeetlem9N  42188  dihmeetlem11N  42190  dihmeetlem12N  42191  dihoml4  42250  djhval  42271  dochexmidlem6  42338  lclkrlem2b  42381  lcfrlem20  42435  lcfrlem23  42438  elrfi  43539  isnacs  43549  mrefg2  43552  mapfzcons2  43564  coeq0i  43598  eldioph2lem2  43606  aomclem8  43902  kelac1  43904  islmodfg  43910  lnr2i  43957  fgraphopab  44044  ntrkbimka  44878  ntrk0kbimka  44879  isotone2  44889  ntrclskb  44909  ntrclsk3  44910  ntrclsk13  44911  neicvgbex  44952  disjrnmpt2  46020  disjinfi  46024  uzinico2  46391  uzinico3  46392  fsumiunss  46405  lptre2pt  46468  limsupresre  46524  limsuplesup  46527  limsupresico  46528  limsupvaluz  46536  limsuplt2  46581  liminfval  46587  limsupge  46589  liminfgval  46590  liminfval2  46596  liminfresico  46599  liminflelimsuplem  46603  liminflelimsup  46604  stoweidlem50  46878  stoweidlem57  46885  subsaliuncllem  47185  sge0val  47194  sge0iunmptlemre  47243  nnfoctbdjlem  47283  iundjiun  47288  vonvolmbllem  47488  smfpimcclem  47635  smfsuplem1  47639  f1cof1blem  47962  3f1oss1  47963  grimuhgr  48803  elbigo  49481  restclsseplem  49841  sepnsepo  49850  aacllem  50772