Theorem ineq2d 4213

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3956

This theorem is referenced by:  rint0  4995  riin0  5086  disji2  5131  disjprgw  5144  disjprg  5145  disjxun  5147  xpriindi  5837  riinint  5968  reseq2  5977  resindm  6031  dfpo2  6296  csbpredg  6307  predep  6332  predprc  6340  predres  6341  onfr  6404  fimacnvinrn  7074  fimacnvinrn2  7075  isofrlem  7337  isoselem  7338  oev2  8523  domss2  9136  funsnfsupp  9387  kmlem11  10155  fpwwe2cbv  10625  fpwwe2lem3  10628  fpwwe2lem7  10632  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  fz1isolem  14422  limsupgle  15421  fsumm1  15697  incexclem  15782  bitsinv1  16383  bitsinvp1  16390  sadcadd  16399  sadadd2  16401  smumullem  16433  ressbas  17179  ressbasOLD  17180  ressress  17193  restval  17372  ismred2  17547  cat1lem  18046  resscatc  18059  cnvps  18531  cntziinsn  19201  lsmdisj3r  19554  lsmdisj3b  19558  gsummptfzsplitl  19801  dmdprd  19868  subgdmdprd  19904  pgpfaclem1  19951  subrgpropd  20355  crng2idl  20877  obselocv  21283  basis1  22453  baspartn  22457  eltg  22460  tgdom  22481  indistopon  22504  ntrval  22540  clslp  22652  resttopon2  22672  restopnb  22679  paste  22798  nrmsep3  22859  imacmp  22901  cmpsub  22904  bwth  22914  llyi  22978  nllyi  22979  cldllycmp  22999  kgencmp2  23050  ptbasfi  23085  kqdisj  23236  kqcldsat  23237  trfbas2  23347  filss  23357  elfg  23375  flimclslem  23488  fcfneii  23541  tsmsfbas  23632  restutopopn  23743  ressxms  24034  restmetu  24079  qtopbaslem  24275  pi1addf  24563  pi1addval  24564  shftmbl  25055  voliunlem1  25067  voliunlem2  25068  uniioombllem2  25100  uniioombllem4  25103  uniioombllem6  25105  volsup2  25122  volcn  25123  volivth  25124  itg1climres  25232  limciun  25411  dvres3a  25431  ig1pval  25690  p1evtxdeqlem  28800  pthdlem2  29056  eupthp1  29500  omlsi  30688  pjoml  30720  chdmj3  30815  chdmj4  30816  ledi  30824  cmbr  30868  cmbr3  30892  pjoml3  30896  fh1  30902  fh2  30903  dmdbr  31583  dmdmd  31584  dmdbr5  31592  dmdsl3  31599  chirredlem2  31675  chirredlem3  31676  dmdbr6ati  31707  unidifsnne  31804  disji2f  31839  disjif2  31843  disjxpin  31850  disjunsn  31856  preiman0  31962  cycpmco2f1  32314  tocyccntz  32334  oppr2idl  32631  isufd  32663  dimkerim  32743  prsss  32927  carsgclctunlem1  33347  carsgclctunlem2  33349  carsgclctunlem3  33350  ballotlemfval  33519  signsplypnf  33592  ftc2re  33641  fsum2dsub  33650  bnj1326  34068  f1resfz0f1d  34134  pthhashvtx  34149  satfv1  34385  satefv  34436  mvrsval  34527  msrfval  34559  mthmpps  34604  elima4  34778  topbnd  35257  opnbnd  35258  cldbnd  35259  neibastop1  35292  neibastop2lem  35293  neibastop2  35294  neibastop3  35295  neifg  35304  bj-ismoored  36036  pibt2  36346  poimirlem3  36539  mblfinlem2  36574  ftc1anclem6  36614  heiborlem3  36729  cnvref4  37267  xrneq2  37298  disjressuc2  37306  elrefrels2  37436  refreleq  37439  elcnvrefrels2  37452  pmodN  38769  polvalN  38824  polatN  38850  trnsetN  39075  djavalN  40054  dihmeetbclemN  40223  dihmeetlem11N  40236  djhval  40317  lclkrlem2e  40430  lcfrlem23  40484  lcdlss2N  40539  metakunt18  41050  metakunt20  41052  elrfi  41480  elrfirn  41481  elrfirn2  41482  eldioph2lem1  41546  conrel2d  42463  ntrkbimka  42837  ntrk0kbimka  42838  isotone2  42848  ntrclskb  42868  ntrclsk3  42869  ntrclsk13  42870  clsneibex  42901  neicvgbex  42911  ismnushort  43108  inabs3  43791  disjiun2  43793  fresin2  43916  lptioo2  44395  lptioo1  44396  limsupvaluz  44472  cncfuni  44650  fourierdlem48  44918  fourierdlem49  44919  fourierdlem93  44963  qndenserrnbllem  45058  nnfoctbdjlem  45219  carageniuncllem1  45285  carageniuncllem2  45286  hoiqssbllem3  45388  smflimlem3  45537  smflim  45541  subrngpropd  46795  restclsseplem  47595