Theorem ineq2d 4176

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-in 3915

This theorem is used by:  rint0  4958  riin0  5053  disji2  5098  disjprg  5110  disjxun  5112  xpriindi  5827  riinint  5967  reseq2  5978  resindmOLD  6035  dfpo2  6304  csbpredg  6315  predep  6338  predprc  6346  predres  6347  onfr  6407  fimacnvinrn  7073  fimacnvinrn2  7074  isofrlem  7349  isoselem  7350  oev2  8517  domss2  9134  funsnfsupp  9362  kmlem11  10163  fpwwe2cbv  10633  fpwwe2lem3  10636  fpwwe2lem7  10640  fpwwe2lem11  10644  fpwwe2lem12  10645  fpwwe2  10646  f1resfz0f1d  13840  fz1isolem  14518  limsupgle  15554  fsumm1  15828  incexclem  15916  bitsinv1  16525  bitsinvp1  16532  sadcadd  16541  sadadd2  16543  smumullem  16575  ressbas  17321  ressress  17332  restval  17504  ismred2  17680  cat1lem  18178  resscatc  18191  cnvps  18659  cntziinsn  19432  lsmdisj3r  19781  lsmdisj3b  19785  gsummptfzsplitl  20028  dmdprd  20095  subgdmdprd  20131  pgpfaclem1  20178  subrngpropd  20697  subrgpropd  20737  crng2idl  21450  obselocv  21908  basis1  23137  baspartn  23141  eltg  23144  tgdom  23165  indistopon  23188  ntrval  23223  clslp  23335  resttopon2  23355  restopnb  23362  paste  23481  nrmsep3  23542  imacmp  23584  cmpsub  23587  bwth  23597  llyi  23661  nllyi  23662  cldllycmp  23682  kgencmp2  23733  ptbasfi  23768  kqdisj  23919  kqcldsat  23920  trfbas2  24030  filss  24040  elfg  24058  flimclslem  24171  fcfneii  24224  tsmsfbas  24315  restutopopn  24425  ressxms  24712  restmetu  24757  qtopbaslem  24945  pi1addf  25236  pi1addval  25237  shftmbl  25727  voliunlem1  25739  voliunlem2  25740  uniioombllem2  25772  uniioombllem4  25775  uniioombllem6  25777  volsup2  25794  volcn  25795  volivth  25796  itg1climres  25903  limciun  26083  dvres3a  26103  ig1pval  26363  p1evtxdeqlem  29892  pthdlem2  30147  eupthp1  30597  omlsi  31786  pjoml  31818  chdmj3  31913  chdmj4  31914  ledi  31922  cmbr  31966  cmbr3  31990  pjoml3  31994  fh1  32000  fh2  32001  dmdbr  32681  dmdmd  32682  dmdbr5  32690  dmdsl3  32697  chirredlem2  32773  chirredlem3  32774  dmdbr6ati  32805  unidifsnne  32912  disji2f  32952  disjif2  32956  disjxpin  32963  disjunsn  32969  preiman0  33085  nn0diffz0  33169  cycpmco2f1  33468  tocyccntz  33488  oppr2idl  33792  isufd  33854  resssra  34001  dimkerim  34041  prsss  34330  carsgclctunlem1  34731  carsgclctunlem2  34733  carsgclctunlem3  34734  ballotlemfval  34904  signsplypnf  34961  ftc2re  35009  fsum2dsub  35018  bnj1326  35438  pthhashvtx  35633  satfv1  35868  satefv  35919  mvrsval  36010  msrfval  36042  mthmpps  36087  elima4  36281  topbnd  36868  opnbnd  36869  cldbnd  36870  neibastop1  36903  neibastop2lem  36904  neibastop2  36905  neibastop3  36906  neifg  36915  dfttc4lem2  37073  bj-ismoored  37782  pibt2  38096  poimirlem3  38307  mblfinlem2  38342  ftc1anclem6  38382  heiborlem3  38497  cnvref4  39032  xrneq2  39081  disjressuc2  39093  elrefrels2  39280  refreleq  39283  elcnvrefrels2  39296  pmodN  40657  polvalN  40712  polatN  40738  trnsetN  40963  djavalN  41942  dihmeetbclemN  42111  dihmeetlem11N  42124  djhval  42205  lclkrlem2e  42318  lcfrlem23  42372  lcdlss2N  42427  elrfi  43458  elrfirn  43459  elrfirn2  43460  eldioph2lem1  43524  conrel2d  44423  ntrkbimka  44797  ntrk0kbimka  44798  isotone2  44808  ntrclskb  44828  ntrclsk3  44829  ntrclsk13  44830  clsneibex  44861  neicvgbex  44871  ismnushort  45044  relpfrlem  45695  inabs3  45809  disjiun2  45811  fresin2  45923  lptioo2  46380  lptioo1  46381  limsupvaluz  46455  cncfuni  46633  fourierdlem48  46901  fourierdlem49  46902  fourierdlem93  46946  qndenserrnbllem  47041  nnfoctbdjlem  47202  carageniuncllem1  47268  carageniuncllem2  47269  hoiqssbllem3  47371  smflimlem3  47520  smflim  47524  resinsnALT  49684  restclsseplem  49726