Theorem ineq2d 4147

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

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3887

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3895

This theorem is referenced by:  rint0  4922  riin0  5012  disji2  5057  disjprgw  5070  disjprg  5071  disjxun  5073  xpriindi  5748  riinint  5880  reseq2  5889  resindm  5943  dfpo2  6203  csbpredg  6212  predep  6237  predprc  6245  predres  6246  onfr  6309  fimacnvinrn  6958  fimacnvinrn2  6959  isofrlem  7220  isoselem  7221  oev2  8362  domss2  8932  funsnfsupp  9161  kmlem11  9925  fpwwe2cbv  10395  fpwwe2lem3  10398  fpwwe2lem7  10402  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  fz1isolem  14184  limsupgle  15195  fsumm1  15472  incexclem  15557  bitsinv1  16158  bitsinvp1  16165  sadcadd  16174  sadadd2  16176  smumullem  16208  ressbas  16956  ressbasOLD  16957  ressress  16967  restval  17146  ismred2  17321  cat1lem  17820  resscatc  17833  cnvps  18305  cntziinsn  18950  lsmdisj3r  19301  lsmdisj3b  19305  gsummptfzsplitl  19543  dmdprd  19610  subgdmdprd  19646  pgpfaclem1  19693  subrgpropd  20068  crng2idl  20519  obselocv  20944  basis1  22109  baspartn  22113  eltg  22116  tgdom  22137  indistopon  22160  ntrval  22196  clslp  22308  resttopon2  22328  restopnb  22335  paste  22454  nrmsep3  22515  imacmp  22557  cmpsub  22560  bwth  22570  llyi  22634  nllyi  22635  cldllycmp  22655  kgencmp2  22706  ptbasfi  22741  kqdisj  22892  kqcldsat  22893  trfbas2  23003  filss  23013  elfg  23031  flimclslem  23144  fcfneii  23197  tsmsfbas  23288  restutopopn  23399  ressxms  23690  restmetu  23735  qtopbaslem  23931  pi1addf  24219  pi1addval  24220  shftmbl  24711  voliunlem1  24723  voliunlem2  24724  uniioombllem2  24756  uniioombllem4  24759  uniioombllem6  24761  volsup2  24778  volcn  24779  volivth  24780  itg1climres  24888  limciun  25067  dvres3a  25087  ig1pval  25346  p1evtxdeqlem  27888  pthdlem2  28145  eupthp1  28589  omlsi  29775  pjoml  29807  chdmj3  29902  chdmj4  29903  ledi  29911  cmbr  29955  cmbr3  29979  pjoml3  29983  fh1  29989  fh2  29990  dmdbr  30670  dmdmd  30671  dmdbr5  30679  dmdsl3  30686  chirredlem2  30762  chirredlem3  30763  dmdbr6ati  30794  unidifsnne  30893  disji2f  30925  disjif2  30929  disjxpin  30936  disjunsn  30942  preiman0  31051  cycpmco2f1  31400  tocyccntz  31420  isufd  31672  dimkerim  31717  prsss  31875  carsgclctunlem1  32293  carsgclctunlem2  32295  carsgclctunlem3  32296  ballotlemfval  32465  signsplypnf  32538  ftc2re  32587  fsum2dsub  32596  bnj1326  33015  f1resfz0f1d  33081  pthhashvtx  33098  satfv1  33334  satefv  33385  mvrsval  33476  msrfval  33508  mthmpps  33553  elima4  33759  topbnd  34522  opnbnd  34523  cldbnd  34524  neibastop1  34557  neibastop2lem  34558  neibastop2  34559  neibastop3  34560  neifg  34569  bj-ismoored  35287  pibt2  35597  poimirlem3  35789  mblfinlem2  35824  ftc1anclem6  35864  heiborlem3  35980  xrneq2  36517  elrefrels2  36642  refreleq  36645  elcnvrefrels2  36655  pmodN  37871  polvalN  37926  polatN  37952  trnsetN  38177  djavalN  39156  dihmeetbclemN  39325  dihmeetlem11N  39338  djhval  39419  lclkrlem2e  39532  lcfrlem23  39586  lcdlss2N  39641  metakunt18  40149  metakunt20  40151  elrfi  40523  elrfirn  40524  elrfirn2  40525  eldioph2lem1  40589  conrel2d  41279  ntrkbimka  41655  ntrk0kbimka  41656  isotone2  41666  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  clsneibex  41719  neicvgbex  41729  ismnushort  41926  inabs3  42611  disjiun2  42613  fresin2  42715  lptioo2  43179  lptioo1  43180  limsupvaluz  43256  cncfuni  43434  fourierdlem48  43702  fourierdlem49  43703  fourierdlem93  43747  qndenserrnbllem  43842  nnfoctbdjlem  44000  carageniuncllem1  44066  carageniuncllem2  44067  hoiqssbllem3  44169  smflimlem3  44318  smflim  44322  restclsseplem  46219