Theorem ineq2d 4120

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094

This theorem is used by:  rint0  4953  riin0  5047  disji2  5092  disjprg  5104  disjxun  5106  xpriindi  5823  riinint  5966  reseq2  5981  resindmOLD  6038  dfpo2  6325  csbpredg  6336  predep  6359  predprc  6367  predres  6368  onfr  6428  fimacnvinrn  7103  fimacnvinrn2  7104  isofrlem  7379  isoselem  7380  oev2  8569  domss2  9193  funsnfsupp  9421  kmlem11  10278  fpwwe2cbv  10754  fpwwe2lem3  10757  fpwwe2lem7  10761  fpwwe2lem11  10765  fpwwe2lem12  10766  fpwwe2  10767  f1resfz0f1d  13967  fz1isolem  14647  limsupgle  15688  fsumm1  15961  incexclem  16049  bitsinv1  16656  bitsinvp1  16663  sadcadd  16672  sadadd2  16674  smumullem  16706  ressbas  17458  ressress  17469  restval  17647  ismred2  17823  cat1lem  18321  resscatc  18334  cnvps  18802  cntziinsn  19602  lsmdisj3r  19951  lsmdisj3b  19955  gsummptfzsplitl  20198  dmdprd  20265  subgdmdprd  20301  pgpfaclem1  20348  subrngpropd  20871  subrgpropd  20911  crng2idl  21627  obselocv  22089  basis1  23323  baspartn  23327  eltg  23330  tgdom  23351  indistopon  23374  ntrval  23409  clslp  23521  resttopon2  23541  restopnb  23548  paste  23667  nrmsep3  23728  imacmp  23770  cmpsub  23773  bwth  23783  llyi  23848  nllyi  23849  cldllycmp  23869  kgencmp2  23920  ptbasfi  23955  kqdisj  24106  kqcldsat  24107  trfbas2  24217  filss  24227  elfg  24245  flimclslem  24358  fcfneii  24411  tsmsfbas  24502  restutopopn  24612  ressxms  24899  restmetu  24944  qtopbaslem  25132  pi1addf  25423  pi1addval  25424  shftmbl  25914  voliunlem1  25926  voliunlem2  25927  uniioombllem2  25959  uniioombllem4  25962  uniioombllem6  25964  volsup2  25981  volcn  25982  volivth  25983  itg1climres  26090  limciun  26269  dvres3a  26289  ig1pval  26549  angmgmaddov1  29445  angmgmaddcl  29448  p1evtxdeqlem  30150  pthhashvtx  30372  pthdlem2  30411  eupthp1  30874  omlsi  32063  pjoml  32095  chdmj3  32190  chdmj4  32191  ledi  32199  cmbr  32243  cmbr3  32267  pjoml3  32271  fh1  32277  fh2  32278  dmdbr  32958  dmdmd  32959  dmdbr5  32967  dmdsl3  32974  chirredlem2  33050  chirredlem3  33051  dmdbr6ati  33082  unidifsnne  33230  disji2f  33269  disjif2  33273  disjxpin  33280  disjunsn  33286  preiman0  33400  nn0diffz0  33482  cycpmco2f1  33784  tocyccntz  33804  oppr2idl  34114  isufd  34176  resssra  34330  dimkerim  34370  prsss  34659  carsgclctunlem1  35060  carsgclctunlem2  35062  carsgclctunlem3  35063  ballotlemfval  35233  signsplypnf  35290  ftc2re  35338  fsum2dsub  35347  bnj1326  35767  gdlop5fv  36008  gdlop6fv  36009  gdlop7fv  36010  gdlop8fv  36011  satfv1  36336  satefv  36387  mvrsval  36478  msrfval  36510  mthmpps  36555  elima4  36755  topbnd  37327  opnbnd  37328  cldbnd  37329  neibastop1  37362  neibastop2lem  37363  neibastop2  37364  neibastop3  37365  neifg  37374  dfttc4lem2  37532  bj-ismoored  38298  pibt2  38608  poimirlem3  38809  mblfinlem2  38844  ftc1anclem6  38884  heiborlem3  39013  cnvref4  39548  xrneq2  39597  disjressuc2  39609  elrefrels2  39796  refreleq  39799  elcnvrefrels2  39812  pmodN  41173  polvalN  41228  polatN  41254  trnsetN  41479  djavalN  42458  dihmeetbclemN  42627  dihmeetlem11N  42640  djhval  42721  lclkrlem2e  42834  lcfrlem23  42888  lcdlss2N  42943  elrfi  43971  elrfirn  43972  elrfirn2  43973  eldioph2lem1  44037  conrel2d  44925  ntrkbimka  45299  ntrk0kbimka  45300  isotone2  45310  ntrclskb  45330  ntrclsk3  45331  ntrclsk13  45332  clsneibex  45363  neicvgbex  45373  ismnushort  45546  relpfrlem  46207  inabs3  46347  disjiun2  46349  fresin2  46460  lptioo2  46916  lptioo1  46917  limsupvaluz  46991  cncfuni  47169  fourierdlem48  47437  fourierdlem49  47438  fourierdlem93  47482  qndenserrnbllem  47577  nnfoctbdjlem  47738  carageniuncllem1  47804  carageniuncllem2  47805  hoiqssbllem3  47907  smflimlem3  48056  smflim  48060  resinsnALT  50317  restclsseplem  50360  parhomco2  51091  parhomco  51092  parmapco2  51103  parmapco  51104