Theorem ineq2d 4179

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

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

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 3403  df-in 3918

This theorem is referenced by:  rint0  4948  riin0  5041  disji2  5086  disjprg  5098  disjxun  5100  xpriindi  5790  riinint  5924  reseq2  5934  resindm  5990  dfpo2  6257  csbpredg  6268  predep  6291  predprc  6299  predres  6300  onfr  6359  fimacnvinrn  7025  fimacnvinrn2  7026  isofrlem  7297  isoselem  7298  oev2  8464  domss2  9077  funsnfsupp  9319  kmlem11  10090  fpwwe2cbv  10559  fpwwe2lem3  10562  fpwwe2lem7  10566  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwe2  10572  fz1isolem  14402  limsupgle  15419  fsumm1  15693  incexclem  15778  bitsinv1  16388  bitsinvp1  16395  sadcadd  16404  sadadd2  16406  smumullem  16438  ressbas  17182  ressress  17193  restval  17365  ismred2  17540  cat1lem  18038  resscatc  18051  cnvps  18519  cntziinsn  19251  lsmdisj3r  19600  lsmdisj3b  19604  gsummptfzsplitl  19847  dmdprd  19914  subgdmdprd  19950  pgpfaclem1  19997  subrngpropd  20488  subrgpropd  20528  crng2idl  21223  obselocv  21670  basis1  22870  baspartn  22874  eltg  22877  tgdom  22898  indistopon  22921  ntrval  22956  clslp  23068  resttopon2  23088  restopnb  23095  paste  23214  nrmsep3  23275  imacmp  23317  cmpsub  23320  bwth  23330  llyi  23394  nllyi  23395  cldllycmp  23415  kgencmp2  23466  ptbasfi  23501  kqdisj  23652  kqcldsat  23653  trfbas2  23763  filss  23773  elfg  23791  flimclslem  23904  fcfneii  23957  tsmsfbas  24048  restutopopn  24159  ressxms  24446  restmetu  24491  qtopbaslem  24679  pi1addf  24980  pi1addval  24981  shftmbl  25472  voliunlem1  25484  voliunlem2  25485  uniioombllem2  25517  uniioombllem4  25520  uniioombllem6  25522  volsup2  25539  volcn  25540  volivth  25541  itg1climres  25648  limciun  25828  dvres3a  25848  ig1pval  26114  p1evtxdeqlem  29493  pthdlem2  29748  eupthp1  30195  omlsi  31383  pjoml  31415  chdmj3  31510  chdmj4  31511  ledi  31519  cmbr  31563  cmbr3  31587  pjoml3  31591  fh1  31597  fh2  31598  dmdbr  32278  dmdmd  32279  dmdbr5  32287  dmdsl3  32294  chirredlem2  32370  chirredlem3  32371  dmdbr6ati  32402  unidifsnne  32515  disji2f  32556  disjif2  32560  disjxpin  32567  disjunsn  32573  preiman0  32683  cycpmco2f1  33096  tocyccntz  33116  oppr2idl  33450  isufd  33504  resssra  33576  dimkerim  33616  prsss  33899  carsgclctunlem1  34301  carsgclctunlem2  34303  carsgclctunlem3  34304  ballotlemfval  34474  signsplypnf  34534  ftc2re  34582  fsum2dsub  34591  bnj1326  35009  f1resfz0f1d  35094  pthhashvtx  35108  satfv1  35343  satefv  35394  mvrsval  35485  msrfval  35517  mthmpps  35562  elima4  35756  topbnd  36305  opnbnd  36306  cldbnd  36307  neibastop1  36340  neibastop2lem  36341  neibastop2  36342  neibastop3  36343  neifg  36352  bj-ismoored  37088  pibt2  37398  poimirlem3  37610  mblfinlem2  37645  ftc1anclem6  37685  heiborlem3  37800  cnvref4  38325  xrneq2  38359  disjressuc2  38367  elrefrels2  38502  refreleq  38505  elcnvrefrels2  38518  pmodN  39837  polvalN  39892  polatN  39918  trnsetN  40143  djavalN  41122  dihmeetbclemN  41291  dihmeetlem11N  41304  djhval  41385  lclkrlem2e  41498  lcfrlem23  41552  lcdlss2N  41607  elrfi  42675  elrfirn  42676  elrfirn2  42677  eldioph2lem1  42741  conrel2d  43646  ntrkbimka  44020  ntrk0kbimka  44021  isotone2  44031  ntrclskb  44051  ntrclsk3  44052  ntrclsk13  44053  clsneibex  44084  neicvgbex  44094  ismnushort  44283  relpfrlem  44936  inabs3  45043  disjiun2  45045  fresin2  45159  lptioo2  45622  lptioo1  45623  limsupvaluz  45699  cncfuni  45877  fourierdlem48  46145  fourierdlem49  46146  fourierdlem93  46190  qndenserrnbllem  46285  nnfoctbdjlem  46446  carageniuncllem1  46512  carageniuncllem2  46513  hoiqssbllem3  46615  smflimlem3  46764  smflim  46768  resinsnALT  48854  restclsseplem  48896