Theorem ineq1d 4070

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

Syntax hints:   → wi 4   = wceq 1507   ∩ cin 3824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-in 3832

This theorem is referenced by:  iinrab2  4852  disji2  4907  disjprg  4919  disjxun  4921  riinint  5674  fnresdisj  6294  fnimadisj  6304  fninfp  6753  ecinxp  8164  fiint  8582  fival  8663  marypha1lem  8684  kmlem12  9373  fin23lem12  9543  fin23lem30  9554  fin23lem33  9557  ttukeylem1  9721  fpwwe2cbv  9842  fpwwe2lem2  9844  fpwwe2  9855  fzval2  12704  fvinim0ffz  12964  limsupval  14682  limsupgval  14684  ello1  14723  elo1  14734  fsum1p  14958  incexclem  15041  fprod1p  15172  smuval2  15681  smueqlem  15689  smumul  15692  setsdm  16363  isacs2  16772  acsfiel  16773  isacs1i  16776  catcval  17204  resscatc  17213  acsficl  17629  lsmdisj3  18557  lsmdisj3a  18563  dprdres  18890  dprdz  18892  dpjdisj  18915  lspdisj2  19611  indistopon  21303  restopnb  21477  ordtrest2  21506  isnrm  21637  cmpcov  21691  cmpsublem  21701  cmpsub  21702  tgcmp  21703  uncmp  21705  hauscmplem  21708  nconnsubb  21725  isnlly  21771  dissnlocfin  21831  kgeni  21839  kgencn3  21860  ptcld  21915  ptcnplem  21923  alexsublem  22346  alexsubb  22348  alexsubALTlem2  22350  alexsubALTlem4  22352  alexsubALT  22353  tmdgsum2  22398  tsmsval2  22431  ustexsym  22517  metrest  22827  qtopbaslem  23060  cnheibor  23252  bndth  23255  lebnumii  23263  iscph  23467  csscld  23545  clsocv  23546  cphsscph  23547  ovolicc2  23816  voliunlem3  23846  ioombl  23859  uniioombllem2  23877  uniioombllem4  23880  uniioombllem6  23882  mbflimsup  23960  taylfval  24640  chtval  25379  ppival  25396  ppival2  25397  ppival2g  25398  chtfl  25418  ppiprm  25420  chtprm  25422  chtnprm  25423  chtdif  25427  ppidif  25432  prmorcht  25447  chdmj2  29078  cmcmlem  29139  pjoml2  29159  fh2  29167  mdbr  29842  mdi  29843  mdbr3  29845  mdbr4  29846  dmdmd  29848  dmdbr3  29853  dmdbr4  29854  dmdi4  29855  dmdbr5  29856  mddmd2  29857  mdsl1i  29869  cvmdi  29872  mdslmd1lem1  29873  mdslmd1lem2  29874  mdslmd1lem3  29875  mdslmd1lem4  29876  mdslmd1i  29877  mdslmd3i  29880  csmdsymi  29882  mdexchi  29883  atomli  29930  atabsi  29949  sumdmdlem2  29967  dmdbr5ati  29970  difuncomp  30063  disji2f  30083  disjif2  30087  disjxpin  30094  disjunsn  30100  fnresin  30125  locfinreflem  30705  iscref  30709  ordtrest2NEW  30767  ordtconnlem1  30768  carsgclctunlem1  31177  totprobd  31287  probmeasb  31291  ballotlemfval  31350  ballotlemfp1  31352  ballotlemgun  31385  chtvalz  31509  bnj1385  31713  bnj1326  31904  iccllysconn  32042  mvrsval  32212  mrsubvrs  32229  mpstval  32242  msubvrs  32267  nosupbnd2lem1  32676  neibastop2lem  33169  neibastop2  33170  neibastop3  33171  limsucncmpi  33253  bj-ismoore  33842  fvineqsnf1  34067  pibt2  34074  ptrest  34280  mblfinlem2  34319  sstotbnd2  34442  cntotbnd  34464  heibor  34489  xrneq1  35022  l1cvat  35584  pmodlem2  36376  pmod2iN  36378  hlmod1i  36385  osumcllem3N  36487  osumcllem9N  36493  pexmidlem6N  36504  pl42lem1N  36508  istrnN  36686  djavalN  37664  dihmeetlem9N  37844  dihmeetlem11N  37846  dihmeetlem12N  37847  dihoml4  37906  djhval  37927  dochexmidlem6  37994  lclkrlem2b  38037  lcfrlem20  38091  lcfrlem23  38094  elrfi  38631  isnacs  38641  mrefg2  38644  mapfzcons2  38656  coeq0i  38690  eldioph2lem2  38698  aomclem8  39002  kelac1  39004  islmodfg  39010  lnr2i  39057  fgraphopab  39151  ntrkbimka  39696  ntrk0kbimka  39697  isotone2  39707  ntrclskb  39727  ntrclsk3  39728  ntrclsk13  39729  neicvgbex  39770  disjrnmpt2  40819  disjinfi  40824  uzinico2  41215  uzinico3  41216  fsumiunss  41233  lptre2pt  41298  limsupresre  41354  limsuplesup  41357  limsupresico  41358  limsupvaluz  41366  limsuplt2  41411  liminfval  41417  limsupge  41419  liminfgval  41420  liminfval2  41426  liminfresico  41429  liminflelimsuplem  41433  liminflelimsup  41434  stoweidlem50  41712  stoweidlem57  41719  subsaliuncllem  42017  sge0val  42025  sge0iunmptlemre  42074  nnfoctbdjlem  42114  iundjiun  42119  vonvolmbllem  42319  smfpimcclem  42458  smfsuplem1  42462  elbigo  43919  aacllem  44209