Theorem ineq2d 4170

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

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-in 3906

This theorem is referenced by:  rint0  4941  riin0  5035  disji2  5080  disjprg  5092  disjxun  5094  xpriindi  5783  riinint  5919  reseq2  5931  resindm  5987  dfpo2  6252  csbpredg  6263  predep  6286  predprc  6294  predres  6295  onfr  6354  fimacnvinrn  7014  fimacnvinrn2  7015  isofrlem  7284  isoselem  7285  oev2  8448  domss2  9062  funsnfsupp  9293  kmlem11  10069  fpwwe2cbv  10539  fpwwe2lem3  10542  fpwwe2lem7  10546  fpwwe2lem11  10550  fpwwe2lem12  10551  fpwwe2  10552  fz1isolem  14382  limsupgle  15398  fsumm1  15672  incexclem  15757  bitsinv1  16367  bitsinvp1  16374  sadcadd  16383  sadadd2  16385  smumullem  16417  ressbas  17161  ressress  17172  restval  17344  ismred2  17520  cat1lem  18018  resscatc  18031  cnvps  18499  cntziinsn  19264  lsmdisj3r  19613  lsmdisj3b  19617  gsummptfzsplitl  19860  dmdprd  19927  subgdmdprd  19963  pgpfaclem1  20010  subrngpropd  20499  subrgpropd  20539  crng2idl  21234  obselocv  21681  basis1  22892  baspartn  22896  eltg  22899  tgdom  22920  indistopon  22943  ntrval  22978  clslp  23090  resttopon2  23110  restopnb  23117  paste  23236  nrmsep3  23297  imacmp  23339  cmpsub  23342  bwth  23352  llyi  23416  nllyi  23417  cldllycmp  23437  kgencmp2  23488  ptbasfi  23523  kqdisj  23674  kqcldsat  23675  trfbas2  23785  filss  23795  elfg  23813  flimclslem  23926  fcfneii  23979  tsmsfbas  24070  restutopopn  24180  ressxms  24467  restmetu  24512  qtopbaslem  24700  pi1addf  25001  pi1addval  25002  shftmbl  25493  voliunlem1  25505  voliunlem2  25506  uniioombllem2  25538  uniioombllem4  25541  uniioombllem6  25543  volsup2  25560  volcn  25561  volivth  25562  itg1climres  25669  limciun  25849  dvres3a  25869  ig1pval  26135  p1evtxdeqlem  29535  pthdlem2  29790  eupthp1  30240  omlsi  31428  pjoml  31460  chdmj3  31555  chdmj4  31556  ledi  31564  cmbr  31608  cmbr3  31632  pjoml3  31636  fh1  31642  fh2  31643  dmdbr  32323  dmdmd  32324  dmdbr5  32332  dmdsl3  32339  chirredlem2  32415  chirredlem3  32416  dmdbr6ati  32447  unidifsnne  32560  disji2f  32601  disjif2  32605  disjxpin  32612  disjunsn  32618  preiman0  32738  nn0diffz0  32823  cycpmco2f1  33155  tocyccntz  33175  oppr2idl  33516  isufd  33570  resssra  33692  dimkerim  33733  prsss  34022  carsgclctunlem1  34423  carsgclctunlem2  34425  carsgclctunlem3  34426  ballotlemfval  34596  signsplypnf  34656  ftc2re  34704  fsum2dsub  34713  bnj1326  35131  f1resfz0f1d  35257  pthhashvtx  35271  satfv1  35506  satefv  35557  mvrsval  35648  msrfval  35680  mthmpps  35725  elima4  35919  topbnd  36467  opnbnd  36468  cldbnd  36469  neibastop1  36502  neibastop2lem  36503  neibastop2  36504  neibastop3  36505  neifg  36514  bj-ismoored  37251  pibt2  37561  poimirlem3  37763  mblfinlem2  37798  ftc1anclem6  37838  heiborlem3  37953  cnvref4  38482  xrneq2  38523  disjressuc2  38535  elrefrels2  38710  refreleq  38713  elcnvrefrels2  38726  pmodN  40049  polvalN  40104  polatN  40130  trnsetN  40355  djavalN  41334  dihmeetbclemN  41503  dihmeetlem11N  41516  djhval  41597  lclkrlem2e  41710  lcfrlem23  41764  lcdlss2N  41819  elrfi  42878  elrfirn  42879  elrfirn2  42880  eldioph2lem1  42944  conrel2d  43847  ntrkbimka  44221  ntrk0kbimka  44222  isotone2  44232  ntrclskb  44252  ntrclsk3  44253  ntrclsk13  44254  clsneibex  44285  neicvgbex  44295  ismnushort  44484  relpfrlem  45136  inabs3  45243  disjiun2  45245  fresin2  45358  lptioo2  45819  lptioo1  45820  limsupvaluz  45894  cncfuni  46072  fourierdlem48  46340  fourierdlem49  46341  fourierdlem93  46385  qndenserrnbllem  46480  nnfoctbdjlem  46641  carageniuncllem1  46707  carageniuncllem2  46708  hoiqssbllem3  46810  smflimlem3  46959  smflim  46963  resinsnALT  49060  restclsseplem  49102