Theorem ineq2d 4241

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

Syntax hints:   → wi 4   = wceq 1537   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  rint0  5012  riin0  5105  disji2  5150  disjprg  5162  disjxun  5164  xpriindi  5861  riinint  5994  reseq2  6004  resindm  6059  dfpo2  6327  csbpredg  6338  predep  6362  predprc  6370  predres  6371  onfr  6434  fimacnvinrn  7105  fimacnvinrn2  7106  isofrlem  7376  isoselem  7377  oev2  8579  domss2  9202  funsnfsupp  9461  kmlem11  10230  fpwwe2cbv  10699  fpwwe2lem3  10702  fpwwe2lem7  10706  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  fz1isolem  14510  limsupgle  15523  fsumm1  15799  incexclem  15884  bitsinv1  16488  bitsinvp1  16495  sadcadd  16504  sadadd2  16506  smumullem  16538  ressbas  17293  ressbasOLD  17294  ressress  17307  restval  17486  ismred2  17661  cat1lem  18163  resscatc  18176  cnvps  18648  cntziinsn  19377  lsmdisj3r  19728  lsmdisj3b  19732  gsummptfzsplitl  19975  dmdprd  20042  subgdmdprd  20078  pgpfaclem1  20125  subrngpropd  20594  subrgpropd  20636  crng2idl  21314  obselocv  21771  basis1  22978  baspartn  22982  eltg  22985  tgdom  23006  indistopon  23029  ntrval  23065  clslp  23177  resttopon2  23197  restopnb  23204  paste  23323  nrmsep3  23384  imacmp  23426  cmpsub  23429  bwth  23439  llyi  23503  nllyi  23504  cldllycmp  23524  kgencmp2  23575  ptbasfi  23610  kqdisj  23761  kqcldsat  23762  trfbas2  23872  filss  23882  elfg  23900  flimclslem  24013  fcfneii  24066  tsmsfbas  24157  restutopopn  24268  ressxms  24559  restmetu  24604  qtopbaslem  24800  pi1addf  25099  pi1addval  25100  shftmbl  25592  voliunlem1  25604  voliunlem2  25605  uniioombllem2  25637  uniioombllem4  25640  uniioombllem6  25642  volsup2  25659  volcn  25660  volivth  25661  itg1climres  25769  limciun  25949  dvres3a  25969  ig1pval  26235  p1evtxdeqlem  29548  pthdlem2  29804  eupthp1  30248  omlsi  31436  pjoml  31468  chdmj3  31563  chdmj4  31564  ledi  31572  cmbr  31616  cmbr3  31640  pjoml3  31644  fh1  31650  fh2  31651  dmdbr  32331  dmdmd  32332  dmdbr5  32340  dmdsl3  32347  chirredlem2  32423  chirredlem3  32424  dmdbr6ati  32455  unidifsnne  32564  disji2f  32599  disjif2  32603  disjxpin  32610  disjunsn  32616  preiman0  32721  cycpmco2f1  33117  tocyccntz  33137  oppr2idl  33479  isufd  33533  resssra  33602  dimkerim  33640  prsss  33862  carsgclctunlem1  34282  carsgclctunlem2  34284  carsgclctunlem3  34285  ballotlemfval  34454  signsplypnf  34527  ftc2re  34575  fsum2dsub  34584  bnj1326  35002  f1resfz0f1d  35081  pthhashvtx  35095  satfv1  35331  satefv  35382  mvrsval  35473  msrfval  35505  mthmpps  35550  elima4  35739  topbnd  36290  opnbnd  36291  cldbnd  36292  neibastop1  36325  neibastop2lem  36326  neibastop2  36327  neibastop3  36328  neifg  36337  bj-ismoored  37073  pibt2  37383  poimirlem3  37583  mblfinlem2  37618  ftc1anclem6  37658  heiborlem3  37773  cnvref4  38306  xrneq2  38336  disjressuc2  38344  elrefrels2  38474  refreleq  38477  elcnvrefrels2  38490  pmodN  39807  polvalN  39862  polatN  39888  trnsetN  40113  djavalN  41092  dihmeetbclemN  41261  dihmeetlem11N  41274  djhval  41355  lclkrlem2e  41468  lcfrlem23  41522  lcdlss2N  41577  metakunt18  42179  metakunt20  42181  elrfi  42650  elrfirn  42651  elrfirn2  42652  eldioph2lem1  42716  conrel2d  43626  ntrkbimka  44000  ntrk0kbimka  44001  isotone2  44011  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  clsneibex  44064  neicvgbex  44074  ismnushort  44270  inabs3  44958  disjiun2  44960  fresin2  45079  lptioo2  45552  lptioo1  45553  limsupvaluz  45629  cncfuni  45807  fourierdlem48  46075  fourierdlem49  46076  fourierdlem93  46120  qndenserrnbllem  46215  nnfoctbdjlem  46376  carageniuncllem1  46442  carageniuncllem2  46443  hoiqssbllem3  46545  smflimlem3  46694  smflim  46698  restclsseplem  48594