Theorem ineq2d 4189

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3943

This theorem is referenced by:  rint0  4916  riin0  5004  disji2  5048  disjprgw  5061  disjprg  5062  disjxun  5064  xpriindi  5707  riinint  5839  reseq2  5848  resindm  5900  predep  6174  onfr  6230  fimacnvinrn  6840  fimacnvinrn2  6841  isofrlem  7093  isoselem  7094  oev2  8148  domss2  8676  funsnfsupp  8857  kmlem11  9586  fpwwe2cbv  10052  fpwwe2lem3  10055  fpwwe2lem8  10059  fpwwe2lem12  10063  fpwwe2lem13  10064  fpwwe2  10065  fz1isolem  13820  limsupgle  14834  fsumm1  15106  incexclem  15191  bitsinv1  15791  bitsinvp1  15798  sadcadd  15807  sadadd2  15809  smumullem  15841  ressbas  16554  ressress  16562  restval  16700  ismred2  16874  resscatc  17365  cnvps  17822  cntziinsn  18465  lsmdisj3r  18812  lsmdisj3b  18816  gsummptfzsplitl  19053  dmdprd  19120  subgdmdprd  19156  pgpfaclem1  19203  subrgpropd  19570  crng2idl  20012  obselocv  20872  basis1  21558  baspartn  21562  eltg  21565  tgdom  21586  indistopon  21609  ntrval  21644  clslp  21756  resttopon2  21776  restopnb  21783  paste  21902  nrmsep3  21963  imacmp  22005  cmpsub  22008  bwth  22018  llyi  22082  nllyi  22083  cldllycmp  22103  kgencmp2  22154  ptbasfi  22189  kqdisj  22340  kqcldsat  22341  trfbas2  22451  filss  22461  elfg  22479  flimclslem  22592  fcfneii  22645  tsmsfbas  22736  restutopopn  22847  ressxms  23135  restmetu  23180  qtopbaslem  23367  pi1addf  23651  pi1addval  23652  shftmbl  24139  voliunlem1  24151  voliunlem2  24152  uniioombllem2  24184  uniioombllem4  24187  uniioombllem6  24189  volsup2  24206  volcn  24207  volivth  24208  itg1climres  24315  limciun  24492  dvres3a  24512  ig1pval  24766  p1evtxdeqlem  27294  pthdlem2  27549  eupthp1  27995  omlsi  29181  pjoml  29213  chdmj3  29308  chdmj4  29309  ledi  29317  cmbr  29361  cmbr3  29385  pjoml3  29389  fh1  29395  fh2  29396  dmdbr  30076  dmdmd  30077  dmdbr5  30085  dmdsl3  30092  chirredlem2  30168  chirredlem3  30169  dmdbr6ati  30200  unidifsnne  30296  disji2f  30327  disjif2  30331  disjxpin  30338  disjunsn  30344  cycpmco2f1  30766  tocyccntz  30786  dimkerim  31023  prsss  31159  carsgclctunlem1  31575  carsgclctunlem2  31577  carsgclctunlem3  31578  ballotlemfval  31747  signsplypnf  31820  ftc2re  31869  fsum2dsub  31878  bnj1326  32298  f1resfz0f1d  32361  pthhashvtx  32374  satfv1  32610  satefv  32661  mvrsval  32752  msrfval  32784  mthmpps  32829  dfpo2  32991  elima4  33019  topbnd  33672  opnbnd  33673  cldbnd  33674  neibastop1  33707  neibastop2lem  33708  neibastop2  33709  neibastop3  33710  neifg  33719  bj-ismoored  34402  csbpredg  34610  pibt2  34701  poimirlem3  34910  mblfinlem2  34945  ftc1anclem6  34987  heiborlem3  35106  xrneq2  35647  elrefrels2  35772  refreleq  35775  elcnvrefrels2  35785  pmodN  37001  polvalN  37056  polatN  37082  trnsetN  37307  djavalN  38286  dihmeetbclemN  38455  dihmeetlem11N  38468  djhval  38549  lclkrlem2e  38662  lcfrlem23  38716  lcdlss2N  38771  elrfi  39311  elrfirn  39312  elrfirn2  39313  eldioph2lem1  39377  conrel2d  40029  ntrkbimka  40408  ntrk0kbimka  40409  isotone2  40419  ntrclskb  40439  ntrclsk3  40440  ntrclsk13  40441  clsneibex  40472  neicvgbex  40482  inabs3  41338  disjiun2  41340  fresin2  41448  lptioo2  41932  lptioo1  41933  limsupvaluz  42009  cncfuni  42189  fourierdlem48  42459  fourierdlem49  42460  fourierdlem93  42504  qndenserrnbllem  42599  nnfoctbdjlem  42757  carageniuncllem1  42823  carageniuncllem2  42824  hoiqssbllem3  42926  smflimlem3  43069  smflim  43073