Theorem ineq2d 4183

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921

This theorem is referenced by:  rint0  4952  riin0  5046  disji2  5091  disjprg  5103  disjxun  5105  xpriindi  5800  riinint  5935  reseq2  5945  resindm  6001  dfpo2  6269  csbpredg  6280  predep  6303  predprc  6311  predres  6312  onfr  6371  fimacnvinrn  7043  fimacnvinrn2  7044  isofrlem  7315  isoselem  7316  oev2  8487  domss2  9100  funsnfsupp  9343  kmlem11  10114  fpwwe2cbv  10583  fpwwe2lem3  10586  fpwwe2lem7  10590  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  fz1isolem  14426  limsupgle  15443  fsumm1  15717  incexclem  15802  bitsinv1  16412  bitsinvp1  16419  sadcadd  16428  sadadd2  16430  smumullem  16462  ressbas  17206  ressress  17217  restval  17389  ismred2  17564  cat1lem  18058  resscatc  18071  cnvps  18537  cntziinsn  19269  lsmdisj3r  19616  lsmdisj3b  19620  gsummptfzsplitl  19863  dmdprd  19930  subgdmdprd  19966  pgpfaclem1  20013  subrngpropd  20477  subrgpropd  20517  crng2idl  21191  obselocv  21637  basis1  22837  baspartn  22841  eltg  22844  tgdom  22865  indistopon  22888  ntrval  22923  clslp  23035  resttopon2  23055  restopnb  23062  paste  23181  nrmsep3  23242  imacmp  23284  cmpsub  23287  bwth  23297  llyi  23361  nllyi  23362  cldllycmp  23382  kgencmp2  23433  ptbasfi  23468  kqdisj  23619  kqcldsat  23620  trfbas2  23730  filss  23740  elfg  23758  flimclslem  23871  fcfneii  23924  tsmsfbas  24015  restutopopn  24126  ressxms  24413  restmetu  24458  qtopbaslem  24646  pi1addf  24947  pi1addval  24948  shftmbl  25439  voliunlem1  25451  voliunlem2  25452  uniioombllem2  25484  uniioombllem4  25487  uniioombllem6  25489  volsup2  25506  volcn  25507  volivth  25508  itg1climres  25615  limciun  25795  dvres3a  25815  ig1pval  26081  p1evtxdeqlem  29440  pthdlem2  29698  eupthp1  30145  omlsi  31333  pjoml  31365  chdmj3  31460  chdmj4  31461  ledi  31469  cmbr  31513  cmbr3  31537  pjoml3  31541  fh1  31547  fh2  31548  dmdbr  32228  dmdmd  32229  dmdbr5  32237  dmdsl3  32244  chirredlem2  32320  chirredlem3  32321  dmdbr6ati  32352  unidifsnne  32465  disji2f  32506  disjif2  32510  disjxpin  32517  disjunsn  32523  preiman0  32633  cycpmco2f1  33081  tocyccntz  33101  oppr2idl  33457  isufd  33511  resssra  33583  dimkerim  33623  prsss  33906  carsgclctunlem1  34308  carsgclctunlem2  34310  carsgclctunlem3  34311  ballotlemfval  34481  signsplypnf  34541  ftc2re  34589  fsum2dsub  34598  bnj1326  35016  f1resfz0f1d  35101  pthhashvtx  35115  satfv1  35350  satefv  35401  mvrsval  35492  msrfval  35524  mthmpps  35569  elima4  35763  topbnd  36312  opnbnd  36313  cldbnd  36314  neibastop1  36347  neibastop2lem  36348  neibastop2  36349  neibastop3  36350  neifg  36359  bj-ismoored  37095  pibt2  37405  poimirlem3  37617  mblfinlem2  37652  ftc1anclem6  37692  heiborlem3  37807  cnvref4  38332  xrneq2  38366  disjressuc2  38374  elrefrels2  38509  refreleq  38512  elcnvrefrels2  38525  pmodN  39844  polvalN  39899  polatN  39925  trnsetN  40150  djavalN  41129  dihmeetbclemN  41298  dihmeetlem11N  41311  djhval  41392  lclkrlem2e  41505  lcfrlem23  41559  lcdlss2N  41614  elrfi  42682  elrfirn  42683  elrfirn2  42684  eldioph2lem1  42748  conrel2d  43653  ntrkbimka  44027  ntrk0kbimka  44028  isotone2  44038  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  clsneibex  44091  neicvgbex  44101  ismnushort  44290  relpfrlem  44943  inabs3  45050  disjiun2  45052  fresin2  45166  lptioo2  45629  lptioo1  45630  limsupvaluz  45706  cncfuni  45884  fourierdlem48  46152  fourierdlem49  46153  fourierdlem93  46197  qndenserrnbllem  46292  nnfoctbdjlem  46453  carageniuncllem1  46519  carageniuncllem2  46520  hoiqssbllem3  46622  smflimlem3  46771  smflim  46775  resinsnALT  48861  restclsseplem  48903