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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906

This theorem is used by:  rint0  4948  riin0  5042  disji2  5087  disjprg  5099  disjxun  5101  xpriindi  5813  riinint  5954  reseq2  5965  resindmOLD  6020  dfpo2  6298  csbpredg  6309  predep  6332  predprc  6340  predres  6341  onfr  6401  fimacnvinrn  7069  fimacnvinrn2  7070  isofrlem  7346  isoselem  7347  oev2  8524  domss2  9148  funsnfsupp  9377  kmlem11  10232  fpwwe2cbv  10708  fpwwe2lem3  10711  fpwwe2lem7  10715  fpwwe2lem11  10719  fpwwe2lem12  10720  fpwwe2  10721  f1resfz0f1d  13920  fz1isolem  14599  limsupgle  15637  fsumm1  15910  incexclem  15998  bitsinv1  16605  bitsinvp1  16612  sadcadd  16621  sadadd2  16623  smumullem  16655  ressbas  17407  ressress  17418  restval  17590  ismred2  17766  cat1lem  18264  resscatc  18277  cnvps  18745  cntziinsn  19544  lsmdisj3r  19893  lsmdisj3b  19897  gsummptfzsplitl  20140  dmdprd  20207  subgdmdprd  20243  pgpfaclem1  20290  subrngpropd  20813  subrgpropd  20853  crng2idl  21569  obselocv  22027  basis1  23261  baspartn  23265  eltg  23268  tgdom  23289  indistopon  23312  ntrval  23347  clslp  23459  resttopon2  23479  restopnb  23486  paste  23605  nrmsep3  23666  imacmp  23708  cmpsub  23711  bwth  23721  llyi  23786  nllyi  23787  cldllycmp  23807  kgencmp2  23858  ptbasfi  23893  kqdisj  24044  kqcldsat  24045  trfbas2  24155  filss  24165  elfg  24183  flimclslem  24296  fcfneii  24349  tsmsfbas  24440  restutopopn  24550  ressxms  24837  restmetu  24882  qtopbaslem  25070  pi1addf  25361  pi1addval  25362  shftmbl  25852  voliunlem1  25864  voliunlem2  25865  uniioombllem2  25897  uniioombllem4  25900  uniioombllem6  25902  volsup2  25919  volcn  25920  volivth  25921  itg1climres  26028  limciun  26207  dvres3a  26227  ig1pval  26487  angmgmaddov1  29381  angmgmaddcl  29384  p1evtxdeqlem  30086  pthhashvtx  30308  pthdlem2  30347  eupthp1  30810  omlsi  31999  pjoml  32031  chdmj3  32126  chdmj4  32127  ledi  32135  cmbr  32179  cmbr3  32203  pjoml3  32207  fh1  32213  fh2  32214  dmdbr  32894  dmdmd  32895  dmdbr5  32903  dmdsl3  32910  chirredlem2  32986  chirredlem3  32987  dmdbr6ati  33018  unidifsnne  33125  disji2f  33164  disjif2  33168  disjxpin  33175  disjunsn  33181  preiman0  33296  nn0diffz0  33379  cycpmco2f1  33678  tocyccntz  33698  oppr2idl  34003  isufd  34065  resssra  34212  dimkerim  34252  prsss  34541  carsgclctunlem1  34942  carsgclctunlem2  34944  carsgclctunlem3  34945  ballotlemfval  35115  signsplypnf  35172  ftc2re  35220  fsum2dsub  35229  bnj1326  35649  satfv1  36107  satefv  36158  mvrsval  36249  msrfval  36281  mthmpps  36326  elima4  36520  topbnd  37092  opnbnd  37093  cldbnd  37094  neibastop1  37127  neibastop2lem  37128  neibastop2  37129  neibastop3  37130  neifg  37139  dfttc4lem2  37297  bj-ismoored  38008  pibt2  38320  poimirlem3  38521  mblfinlem2  38556  ftc1anclem6  38596  heiborlem3  38727  cnvref4  39262  xrneq2  39311  disjressuc2  39323  elrefrels2  39510  refreleq  39513  elcnvrefrels2  39526  pmodN  40887  polvalN  40942  polatN  40968  trnsetN  41193  djavalN  42172  dihmeetbclemN  42341  dihmeetlem11N  42354  djhval  42435  lclkrlem2e  42548  lcfrlem23  42602  lcdlss2N  42657  elrfi  43684  elrfirn  43685  elrfirn2  43686  eldioph2lem1  43750  conrel2d  44649  ntrkbimka  45023  ntrk0kbimka  45024  isotone2  45034  ntrclskb  45054  ntrclsk3  45055  ntrclsk13  45056  clsneibex  45087  neicvgbex  45097  ismnushort  45270  relpfrlem  45921  inabs3  46042  disjiun2  46044  fresin2  46156  lptioo2  46612  lptioo1  46613  limsupvaluz  46687  cncfuni  46865  fourierdlem48  47133  fourierdlem49  47134  fourierdlem93  47178  qndenserrnbllem  47273  nnfoctbdjlem  47434  carageniuncllem1  47500  carageniuncllem2  47501  hoiqssbllem3  47603  smflimlem3  47752  smflim  47756  resinsnALT  49950  restclsseplem  49992