Theorem ineq2d 4186

Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)

Hypothesis

Ref	Expression
ineq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ineq2d	⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Proof of Theorem ineq2d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ineq2 4180	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-in 3924

This theorem is referenced by:  rint0  4955  riin0  5049  disji2  5094  disjprg  5106  disjxun  5108  xpriindi  5803  riinint  5938  reseq2  5948  resindm  6004  dfpo2  6272  csbpredg  6283  predep  6306  predprc  6314  predres  6315  onfr  6374  fimacnvinrn  7046  fimacnvinrn2  7047  isofrlem  7318  isoselem  7319  oev2  8490  domss2  9106  funsnfsupp  9350  kmlem11  10121  fpwwe2cbv  10590  fpwwe2lem3  10593  fpwwe2lem7  10597  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  fz1isolem  14433  limsupgle  15450  fsumm1  15724  incexclem  15809  bitsinv1  16419  bitsinvp1  16426  sadcadd  16435  sadadd2  16437  smumullem  16469  ressbas  17213  ressress  17224  restval  17396  ismred2  17571  cat1lem  18065  resscatc  18078  cnvps  18544  cntziinsn  19276  lsmdisj3r  19623  lsmdisj3b  19627  gsummptfzsplitl  19870  dmdprd  19937  subgdmdprd  19973  pgpfaclem1  20020  subrngpropd  20484  subrgpropd  20524  crng2idl  21198  obselocv  21644  basis1  22844  baspartn  22848  eltg  22851  tgdom  22872  indistopon  22895  ntrval  22930  clslp  23042  resttopon2  23062  restopnb  23069  paste  23188  nrmsep3  23249  imacmp  23291  cmpsub  23294  bwth  23304  llyi  23368  nllyi  23369  cldllycmp  23389  kgencmp2  23440  ptbasfi  23475  kqdisj  23626  kqcldsat  23627  trfbas2  23737  filss  23747  elfg  23765  flimclslem  23878  fcfneii  23931  tsmsfbas  24022  restutopopn  24133  ressxms  24420  restmetu  24465  qtopbaslem  24653  pi1addf  24954  pi1addval  24955  shftmbl  25446  voliunlem1  25458  voliunlem2  25459  uniioombllem2  25491  uniioombllem4  25494  uniioombllem6  25496  volsup2  25513  volcn  25514  volivth  25515  itg1climres  25622  limciun  25802  dvres3a  25822  ig1pval  26088  p1evtxdeqlem  29447  pthdlem2  29705  eupthp1  30152  omlsi  31340  pjoml  31372  chdmj3  31467  chdmj4  31468  ledi  31476  cmbr  31520  cmbr3  31544  pjoml3  31548  fh1  31554  fh2  31555  dmdbr  32235  dmdmd  32236  dmdbr5  32244  dmdsl3  32251  chirredlem2  32327  chirredlem3  32328  dmdbr6ati  32359  unidifsnne  32472  disji2f  32513  disjif2  32517  disjxpin  32524  disjunsn  32530  preiman0  32640  cycpmco2f1  33088  tocyccntz  33108  oppr2idl  33464  isufd  33518  resssra  33590  dimkerim  33630  prsss  33913  carsgclctunlem1  34315  carsgclctunlem2  34317  carsgclctunlem3  34318  ballotlemfval  34488  signsplypnf  34548  ftc2re  34596  fsum2dsub  34605  bnj1326  35023  f1resfz0f1d  35108  pthhashvtx  35122  satfv1  35357  satefv  35408  mvrsval  35499  msrfval  35531  mthmpps  35576  elima4  35770  topbnd  36319  opnbnd  36320  cldbnd  36321  neibastop1  36354  neibastop2lem  36355  neibastop2  36356  neibastop3  36357  neifg  36366  bj-ismoored  37102  pibt2  37412  poimirlem3  37624  mblfinlem2  37659  ftc1anclem6  37699  heiborlem3  37814  cnvref4  38339  xrneq2  38373  disjressuc2  38381  elrefrels2  38516  refreleq  38519  elcnvrefrels2  38532  pmodN  39851  polvalN  39906  polatN  39932  trnsetN  40157  djavalN  41136  dihmeetbclemN  41305  dihmeetlem11N  41318  djhval  41399  lclkrlem2e  41512  lcfrlem23  41566  lcdlss2N  41621  elrfi  42689  elrfirn  42690  elrfirn2  42691  eldioph2lem1  42755  conrel2d  43660  ntrkbimka  44034  ntrk0kbimka  44035  isotone2  44045  ntrclskb  44065  ntrclsk3  44066  ntrclsk13  44067  clsneibex  44098  neicvgbex  44108  ismnushort  44297  relpfrlem  44950  inabs3  45057  disjiun2  45059  fresin2  45173  lptioo2  45636  lptioo1  45637  limsupvaluz  45713  cncfuni  45891  fourierdlem48  46159  fourierdlem49  46160  fourierdlem93  46204  qndenserrnbllem  46299  nnfoctbdjlem  46460  carageniuncllem1  46526  carageniuncllem2  46527  hoiqssbllem3  46629  smflimlem3  46778  smflim  46782  resinsnALT  48865  restclsseplem  48907