Theorem ineq1d 4172

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  iinrab2  5036  disji2  5095  disjprg  5107  disjxun  5109  riinint  5964  fnresdisj  6659  fnimadisj  6671  fninfp  7178  ecinxp  8796  fiint  9293  fival  9379  marypha1lem  9400  kmlem12  10161  fin23lem12  10330  fin23lem30  10341  fin23lem33  10344  ttukeylem1  10508  fpwwe2cbv  10630  fpwwe2lem2  10632  fpwwe2  10643  fzval2  13554  fvinim0ffz  13835  limsupval  15549  limsupgval  15551  ello1  15590  elo1  15601  fsum1p  15827  incexclem  15913  fprod1p  16045  smuval2  16562  smueqlem  16570  smumul  16573  setsdm  17252  isacs2  17731  acsfiel  17732  isacs1i  17735  cat1lem  18175  catcval  18179  resscatc  18188  acsficl  18625  lsmdisj3  19797  lsmdisj3a  19803  dprdres  20144  dprdz  20146  dpjdisj  20169  lspdisj2  21301  indistopon  23208  restopnb  23382  ordtrest2  23411  isnrm  23542  cmpcov  23596  cmpsublem  23606  cmpsub  23607  tgcmp  23608  uncmp  23610  hauscmplem  23613  nconnsubb  23630  isnlly  23677  dissnlocfin  23737  kgeni  23745  kgencn3  23766  ptcld  23821  ptcnplem  23829  alexsublem  24252  alexsubb  24254  alexsubALTlem2  24256  alexsubALTlem4  24258  alexsubALT  24259  tmdgsum2  24304  tsmsval2  24338  ustexsym  24424  metrest  24732  qtopbaslem  24966  cnheibor  25165  bndth  25168  lebnumii  25176  iscph  25380  csscld  25459  clsocv  25460  cphsscph  25461  ovolicc2  25732  voliunlem3  25762  ioombl  25775  uniioombllem2  25793  uniioombllem4  25796  uniioombllem6  25798  mbflimsup  25876  taylfval  26573  chtval  27325  ppival  27342  ppival2  27343  ppival2g  27344  chtfl  27364  ppiprm  27366  chtprm  27368  chtnprm  27369  chtdif  27373  ppidif  27378  prmorcht  27393  nosupbnd2lem1  27930  dfprlng3  29253  dfpth2  30141  chdmj2  31953  cmcmlem  32014  pjoml2  32034  fh2  32042  mdbr  32717  mdi  32718  mdbr3  32720  mdbr4  32721  dmdmd  32723  dmdbr3  32728  dmdbr4  32729  dmdi4  32730  dmdbr5  32731  mddmd2  32732  mdsl1i  32744  cvmdi  32747  mdslmd1lem1  32748  mdslmd1lem2  32749  mdslmd1lem3  32750  mdslmd1lem4  32751  mdslmd1i  32752  mdslmd3i  32755  csmdsymi  32757  mdexchi  32758  atomli  32805  atabsi  32824  sumdmdlem2  32842  dmdbr5ati  32845  difuncomp  32969  disji2f  32993  disjif2  32997  disjxpin  33004  disjunsn  33010  fnresin  33040  cycpmco2f1  33508  cycpmconjslem2  33539  locfinreflem  34294  iscref  34298  ordtrest2NEW  34377  ordtconnlem1  34378  carsgclctunlem1  34772  totprobd  34881  probmeasb  34885  ballotlemfval  34945  ballotlemfp1  34947  ballotlemgun  34980  chtvalz  35081  bnj1385  35285  bnj1326  35479  vonf1wev  35649  vonf1owevOLD  35651  iccllysconn  35779  satfv1  35892  mvrsval  36034  mrsubvrs  36051  mpstval  36064  msubvrs  36089  neibastop2lem  36928  neibastop2  36929  neibastop3  36930  limsucncmpi  37013  dfttc4  37098  mh-infprim2bi  37115  bj-ismoore  37804  fvineqsnf1  38113  pibt2  38120  ptrest  38327  mblfinlem2  38366  sstotbnd2  38483  cntotbnd  38505  heibor  38530  xrneq1  39103  disjressuc2  39118  ecqmap  39156  l1cvat  39887  pmodlem2  40679  pmod2iN  40681  hlmod1i  40688  osumcllem3N  40790  osumcllem9N  40796  pexmidlem6N  40807  pl42lem1N  40811  istrnN  40989  djavalN  41967  dihmeetlem9N  42147  dihmeetlem11N  42149  dihmeetlem12N  42150  dihoml4  42209  djhval  42230  dochexmidlem6  42297  lclkrlem2b  42340  lcfrlem20  42394  lcfrlem23  42397  elrfi  43483  isnacs  43493  mrefg2  43496  mapfzcons2  43508  coeq0i  43542  eldioph2lem2  43550  aomclem8  43846  kelac1  43848  islmodfg  43854  lnr2i  43901  fgraphopab  43988  ntrkbimka  44822  ntrk0kbimka  44823  isotone2  44833  ntrclskb  44853  ntrclsk3  44854  ntrclsk13  44855  neicvgbex  44896  disjrnmpt2  45964  disjinfi  45968  uzinico2  46335  uzinico3  46336  fsumiunss  46349  lptre2pt  46412  limsupresre  46468  limsuplesup  46471  limsupresico  46472  limsupvaluz  46480  limsuplt2  46525  liminfval  46531  limsupge  46533  liminfgval  46534  liminfval2  46540  liminfresico  46543  liminflelimsuplem  46547  liminflelimsup  46548  stoweidlem50  46822  stoweidlem57  46829  subsaliuncllem  47129  sge0val  47138  sge0iunmptlemre  47187  nnfoctbdjlem  47227  iundjiun  47232  vonvolmbllem  47432  smfpimcclem  47579  smfsuplem1  47583  f1cof1blem  47869  3f1oss1  47870  grimuhgr  48710  elbigo  49388  restclsseplem  49750  sepnsepo  49759  aacllem  50678