Theorem ineq2d 4211

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3954

This theorem is referenced by:  rint0  4993  riin0  5084  disji2  5129  disjprgw  5142  disjprg  5143  disjxun  5145  xpriindi  5834  riinint  5965  reseq2  5974  resindm  6028  dfpo2  6292  csbpredg  6303  predep  6328  predprc  6336  predres  6337  onfr  6400  fimacnvinrn  7069  fimacnvinrn2  7070  isofrlem  7332  isoselem  7333  oev2  8518  domss2  9132  funsnfsupp  9383  kmlem11  10151  fpwwe2cbv  10621  fpwwe2lem3  10624  fpwwe2lem7  10628  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  fz1isolem  14418  limsupgle  15417  fsumm1  15693  incexclem  15778  bitsinv1  16379  bitsinvp1  16386  sadcadd  16395  sadadd2  16397  smumullem  16429  ressbas  17175  ressbasOLD  17176  ressress  17189  restval  17368  ismred2  17543  cat1lem  18042  resscatc  18055  cnvps  18527  cntziinsn  19194  lsmdisj3r  19547  lsmdisj3b  19551  gsummptfzsplitl  19793  dmdprd  19860  subgdmdprd  19896  pgpfaclem1  19943  subrgpropd  20388  crng2idl  20864  obselocv  21267  basis1  22435  baspartn  22439  eltg  22442  tgdom  22463  indistopon  22486  ntrval  22522  clslp  22634  resttopon2  22654  restopnb  22661  paste  22780  nrmsep3  22841  imacmp  22883  cmpsub  22886  bwth  22896  llyi  22960  nllyi  22961  cldllycmp  22981  kgencmp2  23032  ptbasfi  23067  kqdisj  23218  kqcldsat  23219  trfbas2  23329  filss  23339  elfg  23357  flimclslem  23470  fcfneii  23523  tsmsfbas  23614  restutopopn  23725  ressxms  24016  restmetu  24061  qtopbaslem  24257  pi1addf  24545  pi1addval  24546  shftmbl  25037  voliunlem1  25049  voliunlem2  25050  uniioombllem2  25082  uniioombllem4  25085  uniioombllem6  25087  volsup2  25104  volcn  25105  volivth  25106  itg1climres  25214  limciun  25393  dvres3a  25413  ig1pval  25672  p1evtxdeqlem  28749  pthdlem2  29005  eupthp1  29449  omlsi  30635  pjoml  30667  chdmj3  30762  chdmj4  30763  ledi  30771  cmbr  30815  cmbr3  30839  pjoml3  30843  fh1  30849  fh2  30850  dmdbr  31530  dmdmd  31531  dmdbr5  31539  dmdsl3  31546  chirredlem2  31622  chirredlem3  31623  dmdbr6ati  31654  unidifsnne  31751  disji2f  31786  disjif2  31790  disjxpin  31797  disjunsn  31803  preiman0  31909  cycpmco2f1  32261  tocyccntz  32281  oppr2idl  32553  isufd  32584  dimkerim  32657  prsss  32834  carsgclctunlem1  33254  carsgclctunlem2  33256  carsgclctunlem3  33257  ballotlemfval  33426  signsplypnf  33499  ftc2re  33548  fsum2dsub  33557  bnj1326  33975  f1resfz0f1d  34041  pthhashvtx  34056  satfv1  34292  satefv  34343  mvrsval  34434  msrfval  34466  mthmpps  34511  elima4  34685  topbnd  35147  opnbnd  35148  cldbnd  35149  neibastop1  35182  neibastop2lem  35183  neibastop2  35184  neibastop3  35185  neifg  35194  bj-ismoored  35926  pibt2  36236  poimirlem3  36429  mblfinlem2  36464  ftc1anclem6  36504  heiborlem3  36619  cnvref4  37157  xrneq2  37188  disjressuc2  37196  elrefrels2  37326  refreleq  37329  elcnvrefrels2  37342  pmodN  38659  polvalN  38714  polatN  38740  trnsetN  38965  djavalN  39944  dihmeetbclemN  40113  dihmeetlem11N  40126  djhval  40207  lclkrlem2e  40320  lcfrlem23  40374  lcdlss2N  40429  metakunt18  40940  metakunt20  40942  elrfi  41365  elrfirn  41366  elrfirn2  41367  eldioph2lem1  41431  conrel2d  42348  ntrkbimka  42722  ntrk0kbimka  42723  isotone2  42733  ntrclskb  42753  ntrclsk3  42754  ntrclsk13  42755  clsneibex  42786  neicvgbex  42796  ismnushort  42993  inabs3  43676  disjiun2  43678  fresin2  43801  lptioo2  44282  lptioo1  44283  limsupvaluz  44359  cncfuni  44537  fourierdlem48  44805  fourierdlem49  44806  fourierdlem93  44850  qndenserrnbllem  44945  nnfoctbdjlem  45106  carageniuncllem1  45172  carageniuncllem2  45173  hoiqssbllem3  45275  smflimlem3  45424  smflim  45428  subrngpropd  46680  restclsseplem  47449