Theorem ineq2d 4173

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-in 3909

This theorem is referenced by:  rint0  4944  riin0  5038  disji2  5083  disjprg  5095  disjxun  5097  xpriindi  5786  riinint  5922  reseq2  5934  resindm  5990  dfpo2  6255  csbpredg  6266  predep  6289  predprc  6297  predres  6298  onfr  6357  fimacnvinrn  7018  fimacnvinrn2  7019  isofrlem  7288  isoselem  7289  oev2  8452  domss2  9068  funsnfsupp  9299  kmlem11  10075  fpwwe2cbv  10545  fpwwe2lem3  10548  fpwwe2lem7  10552  fpwwe2lem11  10556  fpwwe2lem12  10557  fpwwe2  10558  fz1isolem  14388  limsupgle  15404  fsumm1  15678  incexclem  15763  bitsinv1  16373  bitsinvp1  16380  sadcadd  16389  sadadd2  16391  smumullem  16423  ressbas  17167  ressress  17178  restval  17350  ismred2  17526  cat1lem  18024  resscatc  18037  cnvps  18505  cntziinsn  19270  lsmdisj3r  19619  lsmdisj3b  19623  gsummptfzsplitl  19866  dmdprd  19933  subgdmdprd  19969  pgpfaclem1  20016  subrngpropd  20505  subrgpropd  20545  crng2idl  21240  obselocv  21687  basis1  22898  baspartn  22902  eltg  22905  tgdom  22926  indistopon  22949  ntrval  22984  clslp  23096  resttopon2  23116  restopnb  23123  paste  23242  nrmsep3  23303  imacmp  23345  cmpsub  23348  bwth  23358  llyi  23422  nllyi  23423  cldllycmp  23443  kgencmp2  23494  ptbasfi  23529  kqdisj  23680  kqcldsat  23681  trfbas2  23791  filss  23801  elfg  23819  flimclslem  23932  fcfneii  23985  tsmsfbas  24076  restutopopn  24186  ressxms  24473  restmetu  24518  qtopbaslem  24706  pi1addf  25007  pi1addval  25008  shftmbl  25499  voliunlem1  25511  voliunlem2  25512  uniioombllem2  25544  uniioombllem4  25547  uniioombllem6  25549  volsup2  25566  volcn  25567  volivth  25568  itg1climres  25675  limciun  25855  dvres3a  25875  ig1pval  26141  p1evtxdeqlem  29569  pthdlem2  29824  eupthp1  30274  omlsi  31462  pjoml  31494  chdmj3  31589  chdmj4  31590  ledi  31598  cmbr  31642  cmbr3  31666  pjoml3  31670  fh1  31676  fh2  31677  dmdbr  32357  dmdmd  32358  dmdbr5  32366  dmdsl3  32373  chirredlem2  32449  chirredlem3  32450  dmdbr6ati  32481  unidifsnne  32593  disji2f  32634  disjif2  32638  disjxpin  32645  disjunsn  32651  preiman0  32770  nn0diffz0  32855  cycpmco2f1  33187  tocyccntz  33207  oppr2idl  33548  isufd  33602  resssra  33724  dimkerim  33765  prsss  34054  carsgclctunlem1  34455  carsgclctunlem2  34457  carsgclctunlem3  34458  ballotlemfval  34628  signsplypnf  34688  ftc2re  34736  fsum2dsub  34745  bnj1326  35163  f1resfz0f1d  35289  pthhashvtx  35303  satfv1  35538  satefv  35589  mvrsval  35680  msrfval  35712  mthmpps  35757  elima4  35951  topbnd  36499  opnbnd  36500  cldbnd  36501  neibastop1  36534  neibastop2lem  36535  neibastop2  36536  neibastop3  36537  neifg  36546  bj-ismoored  37283  pibt2  37593  poimirlem3  37795  mblfinlem2  37830  ftc1anclem6  37870  heiborlem3  37985  cnvref4  38522  xrneq2  38571  disjressuc2  38583  elrefrels2  38770  refreleq  38773  elcnvrefrels2  38786  pmodN  40147  polvalN  40202  polatN  40228  trnsetN  40453  djavalN  41432  dihmeetbclemN  41601  dihmeetlem11N  41614  djhval  41695  lclkrlem2e  41808  lcfrlem23  41862  lcdlss2N  41917  elrfi  42972  elrfirn  42973  elrfirn2  42974  eldioph2lem1  43038  conrel2d  43941  ntrkbimka  44315  ntrk0kbimka  44316  isotone2  44326  ntrclskb  44346  ntrclsk3  44347  ntrclsk13  44348  clsneibex  44379  neicvgbex  44389  ismnushort  44578  relpfrlem  45230  inabs3  45337  disjiun2  45339  fresin2  45452  lptioo2  45913  lptioo1  45914  limsupvaluz  45988  cncfuni  46166  fourierdlem48  46434  fourierdlem49  46435  fourierdlem93  46479  qndenserrnbllem  46574  nnfoctbdjlem  46735  carageniuncllem1  46801  carageniuncllem2  46802  hoiqssbllem3  46904  smflimlem3  47053  smflim  47057  resinsnALT  49154  restclsseplem  49196