Theorem ineq2d 4166

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  rint0  4948  riin0  5042  disji2  5087  disjprg  5099  disjxun  5101  xpriindi  5816  riinint  5956  reseq2  5967  resindmOLD  6024  dfpo2  6294  csbpredg  6305  predep  6328  predprc  6336  predres  6337  onfr  6397  fimacnvinrn  7064  fimacnvinrn2  7065  isofrlem  7341  isoselem  7342  oev2  8510  domss2  9134  funsnfsupp  9362  kmlem11  10163  fpwwe2cbv  10639  fpwwe2lem3  10642  fpwwe2lem7  10646  fpwwe2lem11  10650  fpwwe2lem12  10651  fpwwe2  10652  f1resfz0f1d  13848  fz1isolem  14526  limsupgle  15564  fsumm1  15837  incexclem  15925  bitsinv1  16532  bitsinvp1  16539  sadcadd  16548  sadadd2  16550  smumullem  16582  ressbas  17328  ressress  17339  restval  17511  ismred2  17687  cat1lem  18185  resscatc  18198  cnvps  18666  cntziinsn  19464  lsmdisj3r  19813  lsmdisj3b  19817  gsummptfzsplitl  20060  dmdprd  20127  subgdmdprd  20163  pgpfaclem1  20210  subrngpropd  20730  subrgpropd  20770  crng2idl  21483  obselocv  21941  basis1  23175  baspartn  23179  eltg  23182  tgdom  23203  indistopon  23226  ntrval  23261  clslp  23373  resttopon2  23393  restopnb  23400  paste  23519  nrmsep3  23580  imacmp  23622  cmpsub  23625  bwth  23635  llyi  23700  nllyi  23701  cldllycmp  23721  kgencmp2  23772  ptbasfi  23807  kqdisj  23958  kqcldsat  23959  trfbas2  24069  filss  24079  elfg  24097  flimclslem  24210  fcfneii  24263  tsmsfbas  24354  restutopopn  24464  ressxms  24751  restmetu  24796  qtopbaslem  24984  pi1addf  25275  pi1addval  25276  shftmbl  25766  voliunlem1  25778  voliunlem2  25779  uniioombllem2  25811  uniioombllem4  25814  uniioombllem6  25816  volsup2  25833  volcn  25834  volivth  25835  itg1climres  25942  limciun  26121  dvres3a  26141  ig1pval  26401  angmgmaddov1  29267  angmgmaddcl  29270  p1evtxdeqlem  29972  pthhashvtx  30194  pthdlem2  30233  eupthp1  30696  omlsi  31885  pjoml  31917  chdmj3  32012  chdmj4  32013  ledi  32021  cmbr  32065  cmbr3  32089  pjoml3  32093  fh1  32099  fh2  32100  dmdbr  32780  dmdmd  32781  dmdbr5  32789  dmdsl3  32796  chirredlem2  32872  chirredlem3  32873  dmdbr6ati  32904  unidifsnne  33011  disji2f  33050  disjif2  33054  disjxpin  33061  disjunsn  33067  preiman0  33182  nn0diffz0  33265  cycpmco2f1  33564  tocyccntz  33584  oppr2idl  33888  isufd  33950  resssra  34097  dimkerim  34137  prsss  34426  carsgclctunlem1  34828  carsgclctunlem2  34830  carsgclctunlem3  34831  ballotlemfval  35001  signsplypnf  35058  ftc2re  35106  fsum2dsub  35115  bnj1326  35535  satfv1  35942  satefv  35993  mvrsval  36084  msrfval  36116  mthmpps  36161  elima4  36355  topbnd  36943  opnbnd  36944  cldbnd  36945  neibastop1  36978  neibastop2lem  36979  neibastop2  36980  neibastop3  36981  neifg  36990  dfttc4lem2  37148  bj-ismoored  37857  pibt2  38171  poimirlem3  38372  mblfinlem2  38407  ftc1anclem6  38447  heiborlem3  38563  cnvref4  39098  xrneq2  39147  disjressuc2  39159  elrefrels2  39346  refreleq  39349  elcnvrefrels2  39362  pmodN  40723  polvalN  40778  polatN  40804  trnsetN  41029  djavalN  42008  dihmeetbclemN  42177  dihmeetlem11N  42190  djhval  42271  lclkrlem2e  42384  lcfrlem23  42438  lcdlss2N  42493  elrfi  43539  elrfirn  43540  elrfirn2  43541  eldioph2lem1  43605  conrel2d  44504  ntrkbimka  44878  ntrk0kbimka  44879  isotone2  44889  ntrclskb  44909  ntrclsk3  44910  ntrclsk13  44911  clsneibex  44942  neicvgbex  44952  ismnushort  45125  relpfrlem  45776  inabs3  45890  disjiun2  45892  fresin2  46004  lptioo2  46461  lptioo1  46462  limsupvaluz  46536  cncfuni  46714  fourierdlem48  46982  fourierdlem49  46983  fourierdlem93  47027  qndenserrnbllem  47122  nnfoctbdjlem  47283  carageniuncllem1  47349  carageniuncllem2  47350  hoiqssbllem3  47452  smflimlem3  47601  smflim  47605  resinsnALT  49799  restclsseplem  49841