Theorem ineq2d 4195

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-in 3933

This theorem is referenced by:  rint0  4964  riin0  5058  disji2  5103  disjprg  5115  disjxun  5117  xpriindi  5816  riinint  5951  reseq2  5961  resindm  6017  dfpo2  6285  csbpredg  6296  predep  6319  predprc  6327  predres  6328  onfr  6391  fimacnvinrn  7061  fimacnvinrn2  7062  isofrlem  7333  isoselem  7334  oev2  8535  domss2  9150  funsnfsupp  9404  kmlem11  10175  fpwwe2cbv  10644  fpwwe2lem3  10647  fpwwe2lem7  10651  fpwwe2lem11  10655  fpwwe2lem12  10656  fpwwe2  10657  fz1isolem  14479  limsupgle  15493  fsumm1  15767  incexclem  15852  bitsinv1  16461  bitsinvp1  16468  sadcadd  16477  sadadd2  16479  smumullem  16511  ressbas  17257  ressress  17268  restval  17440  ismred2  17615  cat1lem  18109  resscatc  18122  cnvps  18588  cntziinsn  19320  lsmdisj3r  19667  lsmdisj3b  19671  gsummptfzsplitl  19914  dmdprd  19981  subgdmdprd  20017  pgpfaclem1  20064  subrngpropd  20528  subrgpropd  20568  crng2idl  21242  obselocv  21688  basis1  22888  baspartn  22892  eltg  22895  tgdom  22916  indistopon  22939  ntrval  22974  clslp  23086  resttopon2  23106  restopnb  23113  paste  23232  nrmsep3  23293  imacmp  23335  cmpsub  23338  bwth  23348  llyi  23412  nllyi  23413  cldllycmp  23433  kgencmp2  23484  ptbasfi  23519  kqdisj  23670  kqcldsat  23671  trfbas2  23781  filss  23791  elfg  23809  flimclslem  23922  fcfneii  23975  tsmsfbas  24066  restutopopn  24177  ressxms  24464  restmetu  24509  qtopbaslem  24697  pi1addf  24998  pi1addval  24999  shftmbl  25491  voliunlem1  25503  voliunlem2  25504  uniioombllem2  25536  uniioombllem4  25539  uniioombllem6  25541  volsup2  25558  volcn  25559  volivth  25560  itg1climres  25667  limciun  25847  dvres3a  25867  ig1pval  26133  p1evtxdeqlem  29492  pthdlem2  29750  eupthp1  30197  omlsi  31385  pjoml  31417  chdmj3  31512  chdmj4  31513  ledi  31521  cmbr  31565  cmbr3  31589  pjoml3  31593  fh1  31599  fh2  31600  dmdbr  32280  dmdmd  32281  dmdbr5  32289  dmdsl3  32296  chirredlem2  32372  chirredlem3  32373  dmdbr6ati  32404  unidifsnne  32517  disji2f  32558  disjif2  32562  disjxpin  32569  disjunsn  32575  preiman0  32687  cycpmco2f1  33135  tocyccntz  33155  oppr2idl  33501  isufd  33555  resssra  33627  dimkerim  33667  prsss  33947  carsgclctunlem1  34349  carsgclctunlem2  34351  carsgclctunlem3  34352  ballotlemfval  34522  signsplypnf  34582  ftc2re  34630  fsum2dsub  34639  bnj1326  35057  f1resfz0f1d  35136  pthhashvtx  35150  satfv1  35385  satefv  35436  mvrsval  35527  msrfval  35559  mthmpps  35604  elima4  35793  topbnd  36342  opnbnd  36343  cldbnd  36344  neibastop1  36377  neibastop2lem  36378  neibastop2  36379  neibastop3  36380  neifg  36389  bj-ismoored  37125  pibt2  37435  poimirlem3  37647  mblfinlem2  37682  ftc1anclem6  37722  heiborlem3  37837  cnvref4  38368  xrneq2  38398  disjressuc2  38406  elrefrels2  38536  refreleq  38539  elcnvrefrels2  38552  pmodN  39869  polvalN  39924  polatN  39950  trnsetN  40175  djavalN  41154  dihmeetbclemN  41323  dihmeetlem11N  41336  djhval  41417  lclkrlem2e  41530  lcfrlem23  41584  lcdlss2N  41639  metakunt18  42235  metakunt20  42237  elrfi  42717  elrfirn  42718  elrfirn2  42719  eldioph2lem1  42783  conrel2d  43688  ntrkbimka  44062  ntrk0kbimka  44063  isotone2  44073  ntrclskb  44093  ntrclsk3  44094  ntrclsk13  44095  clsneibex  44126  neicvgbex  44136  ismnushort  44325  relpfrlem  44978  inabs3  45080  disjiun2  45082  fresin2  45196  lptioo2  45660  lptioo1  45661  limsupvaluz  45737  cncfuni  45915  fourierdlem48  46183  fourierdlem49  46184  fourierdlem93  46228  qndenserrnbllem  46323  nnfoctbdjlem  46484  carageniuncllem1  46550  carageniuncllem2  46551  hoiqssbllem3  46653  smflimlem3  46802  smflim  46806  resinsnALT  48848  restclsseplem  48889