Theorem ineq2d 3814

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

Syntax hints:   → wi 4   = wceq 1483   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  disjpr2OLD  4249  rint0  4517  riin0  4594  disji2  4636  disjprg  4648  disjxun  4651  xpriindi  5258  riinint  5382  reseq2  5391  resindm  5444  predep  5706  onfr  5763  fimacnvinrn  6348  fimacnvinrn2  6349  isofrlem  6590  isoselem  6591  oev2  7603  domss2  8119  funsnfsupp  8299  kmlem11  8982  fpwwe2cbv  9452  fpwwe2lem3  9455  fpwwe2lem8  9459  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  fz1isolem  13245  limsupgle  14208  fsumm1  14480  incexclem  14568  bitsinv1  15164  bitsinvp1  15171  sadcadd  15180  sadadd2  15182  smumullem  15214  ressbas  15930  ressress  15938  restval  16087  ismred2  16263  resscatc  16755  cnvps  17212  cntziinsn  17767  lsmdisj3r  18099  lsmdisj3b  18103  gsummptfzsplitl  18333  dmdprd  18397  subgdmdprd  18433  pgpfaclem1  18480  subrgpropd  18814  crng2idl  19239  obselocv  20072  basis1  20754  baspartn  20758  eltg  20761  tgdom  20782  indistopon  20805  ntrval  20840  clslp  20952  resttopon2  20972  restopnb  20979  paste  21098  nrmsep3  21159  imacmp  21200  cmpsub  21203  bwth  21213  llyi  21277  nllyi  21278  cldllycmp  21298  kgencmp2  21349  ptbasfi  21384  kqdisj  21535  kqcldsat  21536  trfbas2  21647  filss  21657  elfg  21675  flimclslem  21788  fcfneii  21841  tsmsfbas  21931  restutopopn  22042  ressxms  22330  restmetu  22375  qtopbaslem  22562  pi1addf  22847  pi1addval  22848  shftmbl  23306  voliunlem1  23318  voliunlem2  23319  uniioombllem2  23351  uniioombllem4  23354  uniioombllem6  23356  volsup2  23373  volcn  23374  volivth  23375  itg1climres  23481  limciun  23658  dvres3a  23678  ig1pval  23932  p1evtxdeqlem  26408  pthdlem2  26664  eupthp1  27076  omlsi  28263  pjoml  28295  chdmj3  28390  chdmj4  28391  ledi  28399  cmbr  28443  cmbr3  28467  pjoml3  28471  fh1  28477  fh2  28478  dmdbr  29158  dmdmd  29159  dmdbr5  29167  dmdsl3  29174  chirredlem2  29250  chirredlem3  29251  dmdbr6ati  29282  disji2f  29390  disjif2  29394  disjxpin  29401  disjunsn  29407  prsss  29962  carsgclctunlem1  30379  carsgclctunlem2  30381  carsgclctunlem3  30382  ballotlemfval  30551  signsplypnf  30627  ftc2re  30676  fsum2dsub  30685  bnj1326  31094  mvrsval  31402  msrfval  31434  mthmpps  31479  dfpo2  31645  elima4  31679  topbnd  32319  opnbnd  32320  cldbnd  32321  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  neibastop3  32357  neifg  32366  bj-ismoored  33062  bj-diagval  33090  csbpredg  33172  poimirlem3  33412  mblfinlem2  33447  ftc1anclem6  33490  heiborlem3  33612  pmodN  35136  polvalN  35191  polatN  35217  trnsetN  35443  djavalN  36424  dihmeetbclemN  36593  dihmeetlem11N  36606  djhval  36687  lclkrlem2e  36800  lcfrlem23  36854  lcdlss2N  36909  elrfi  37257  elrfirn  37258  elrfirn2  37259  eldioph2lem1  37323  conrel2d  37956  ntrkbimka  38336  ntrk0kbimka  38337  isotone2  38347  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  clsneibex  38400  neicvgbex  38410  csbresgOLD  39055  inabs3  39224  disjiun2  39226  fresin2  39352  lptioo2  39863  lptioo1  39864  limsupvaluz  39940  cncfuni  40099  fourierdlem48  40371  fourierdlem49  40372  fourierdlem93  40416  qndenserrnbllem  40514  nnfoctbdjlem  40672  carageniuncllem1  40735  carageniuncllem2  40736  hoiqssbllem3  40838  smflimlem3  40981  smflim  40985