Theorem ineq2d 4116

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4090

This theorem is used by:  rint0  4947  riin0  5041  disji2  5086  disjprg  5098  disjxun  5100  xpriindi  5814  riinint  5955  reseq2  5966  resindmOLD  6022  dfpo2  6302  csbpredg  6313  predep  6336  predprc  6344  predres  6345  onfr  6405  fimacnvinrn  7076  fimacnvinrn2  7077  isofrlem  7352  isoselem  7353  oev2  8538  domss2  9162  funsnfsupp  9391  kmlem11  10246  fpwwe2cbv  10722  fpwwe2lem3  10725  fpwwe2lem7  10729  fpwwe2lem11  10733  fpwwe2lem12  10734  fpwwe2  10735  f1resfz0f1d  13934  fz1isolem  14613  limsupgle  15653  fsumm1  15926  incexclem  16014  bitsinv1  16621  bitsinvp1  16628  sadcadd  16637  sadadd2  16639  smumullem  16671  ressbas  17423  ressress  17434  restval  17606  ismred2  17782  cat1lem  18280  resscatc  18293  cnvps  18761  cntziinsn  19560  lsmdisj3r  19909  lsmdisj3b  19913  gsummptfzsplitl  20156  dmdprd  20223  subgdmdprd  20259  pgpfaclem1  20306  subrngpropd  20829  subrgpropd  20869  crng2idl  21585  obselocv  22043  basis1  23277  baspartn  23281  eltg  23284  tgdom  23305  indistopon  23328  ntrval  23363  clslp  23475  resttopon2  23495  restopnb  23502  paste  23621  nrmsep3  23682  imacmp  23724  cmpsub  23727  bwth  23737  llyi  23802  nllyi  23803  cldllycmp  23823  kgencmp2  23874  ptbasfi  23909  kqdisj  24060  kqcldsat  24061  trfbas2  24171  filss  24181  elfg  24199  flimclslem  24312  fcfneii  24365  tsmsfbas  24456  restutopopn  24566  ressxms  24853  restmetu  24898  qtopbaslem  25086  pi1addf  25377  pi1addval  25378  shftmbl  25868  voliunlem1  25880  voliunlem2  25881  uniioombllem2  25913  uniioombllem4  25916  uniioombllem6  25918  volsup2  25935  volcn  25936  volivth  25937  itg1climres  26044  limciun  26223  dvres3a  26243  ig1pval  26503  angmgmaddov1  29397  angmgmaddcl  29400  p1evtxdeqlem  30102  pthhashvtx  30324  pthdlem2  30363  eupthp1  30826  omlsi  32015  pjoml  32047  chdmj3  32142  chdmj4  32143  ledi  32151  cmbr  32195  cmbr3  32219  pjoml3  32223  fh1  32229  fh2  32230  dmdbr  32910  dmdmd  32911  dmdbr5  32919  dmdsl3  32926  chirredlem2  33002  chirredlem3  33003  dmdbr6ati  33034  unidifsnne  33183  disji2f  33222  disjif2  33226  disjxpin  33233  disjunsn  33239  preiman0  33354  nn0diffz0  33436  cycpmco2f1  33735  tocyccntz  33755  oppr2idl  34060  isufd  34122  resssra  34269  dimkerim  34309  prsss  34598  carsgclctunlem1  34999  carsgclctunlem2  35001  carsgclctunlem3  35002  ballotlemfval  35172  signsplypnf  35229  ftc2re  35277  fsum2dsub  35286  bnj1326  35706  satfv1  36218  satefv  36269  mvrsval  36360  msrfval  36392  mthmpps  36437  elima4  36636  topbnd  37208  opnbnd  37209  cldbnd  37210  neibastop1  37243  neibastop2lem  37244  neibastop2  37245  neibastop3  37246  neifg  37255  dfttc4lem2  37413  bj-ismoored  38136  pibt2  38449  poimirlem3  38650  mblfinlem2  38685  ftc1anclem6  38725  heiborlem3  38856  cnvref4  39391  xrneq2  39440  disjressuc2  39452  elrefrels2  39639  refreleq  39642  elcnvrefrels2  39655  pmodN  41016  polvalN  41071  polatN  41097  trnsetN  41322  djavalN  42301  dihmeetbclemN  42470  dihmeetlem11N  42483  djhval  42564  lclkrlem2e  42677  lcfrlem23  42731  lcdlss2N  42786  elrfi  43814  elrfirn  43815  elrfirn2  43816  eldioph2lem1  43880  conrel2d  44773  ntrkbimka  45147  ntrk0kbimka  45148  isotone2  45158  ntrclskb  45178  ntrclsk3  45179  ntrclsk13  45180  clsneibex  45211  neicvgbex  45221  ismnushort  45394  relpfrlem  46051  inabs3  46181  disjiun2  46183  fresin2  46295  lptioo2  46751  lptioo1  46752  limsupvaluz  46826  cncfuni  47004  fourierdlem48  47272  fourierdlem49  47273  fourierdlem93  47317  qndenserrnbllem  47412  nnfoctbdjlem  47573  carageniuncllem1  47639  carageniuncllem2  47640  hoiqssbllem3  47742  smflimlem3  47891  smflim  47895  resinsnALT  50094  restclsseplem  50137  parhomco2  50868  parhomco  50869  parmapco2  50880  parmapco  50881