Theorem ineq2d 4173

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

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

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 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  rint0  4955  riin0  5050  disji2  5095  disjprg  5107  disjxun  5109  xpriindi  5824  riinint  5964  reseq2  5975  resindmOLD  6032  dfpo2  6301  csbpredg  6312  predep  6335  predprc  6343  predres  6344  onfr  6404  fimacnvinrn  7070  fimacnvinrn2  7071  isofrlem  7347  isoselem  7348  oev2  8514  domss2  9131  funsnfsupp  9359  kmlem11  10160  fpwwe2cbv  10630  fpwwe2lem3  10633  fpwwe2lem7  10637  fpwwe2lem11  10641  fpwwe2lem12  10642  fpwwe2  10643  f1resfz0f1d  13838  fz1isolem  14516  limsupgle  15552  fsumm1  15825  incexclem  15913  bitsinv1  16522  bitsinvp1  16529  sadcadd  16538  sadadd2  16540  smumullem  16572  ressbas  17318  ressress  17329  restval  17501  ismred2  17677  cat1lem  18175  resscatc  18188  cnvps  18656  cntziinsn  19451  lsmdisj3r  19800  lsmdisj3b  19804  gsummptfzsplitl  20047  dmdprd  20114  subgdmdprd  20150  pgpfaclem1  20197  subrngpropd  20717  subrgpropd  20757  crng2idl  21470  obselocv  21928  basis1  23157  baspartn  23161  eltg  23164  tgdom  23185  indistopon  23208  ntrval  23243  clslp  23355  resttopon2  23375  restopnb  23382  paste  23501  nrmsep3  23562  imacmp  23604  cmpsub  23607  bwth  23617  llyi  23682  nllyi  23683  cldllycmp  23703  kgencmp2  23754  ptbasfi  23789  kqdisj  23940  kqcldsat  23941  trfbas2  24051  filss  24061  elfg  24079  flimclslem  24192  fcfneii  24245  tsmsfbas  24336  restutopopn  24446  ressxms  24733  restmetu  24778  qtopbaslem  24966  pi1addf  25257  pi1addval  25258  shftmbl  25748  voliunlem1  25760  voliunlem2  25761  uniioombllem2  25793  uniioombllem4  25796  uniioombllem6  25798  volsup2  25815  volcn  25816  volivth  25817  itg1climres  25924  limciun  26104  dvres3a  26124  ig1pval  26384  p1evtxdeqlem  29920  pthhashvtx  30142  pthdlem2  30181  eupthp1  30638  omlsi  31827  pjoml  31859  chdmj3  31954  chdmj4  31955  ledi  31963  cmbr  32007  cmbr3  32031  pjoml3  32035  fh1  32041  fh2  32042  dmdbr  32722  dmdmd  32723  dmdbr5  32731  dmdsl3  32738  chirredlem2  32814  chirredlem3  32815  dmdbr6ati  32846  unidifsnne  32953  disji2f  32993  disjif2  32997  disjxpin  33004  disjunsn  33010  preiman0  33126  nn0diffz0  33209  cycpmco2f1  33508  tocyccntz  33528  oppr2idl  33832  isufd  33894  resssra  34041  dimkerim  34081  prsss  34370  carsgclctunlem1  34772  carsgclctunlem2  34774  carsgclctunlem3  34775  ballotlemfval  34945  signsplypnf  35002  ftc2re  35050  fsum2dsub  35059  bnj1326  35479  satfv1  35892  satefv  35943  mvrsval  36034  msrfval  36066  mthmpps  36111  elima4  36305  topbnd  36892  opnbnd  36893  cldbnd  36894  neibastop1  36927  neibastop2lem  36928  neibastop2  36929  neibastop3  36930  neifg  36939  dfttc4lem2  37097  bj-ismoored  37806  pibt2  38120  poimirlem3  38331  mblfinlem2  38366  ftc1anclem6  38406  heiborlem3  38522  cnvref4  39057  xrneq2  39106  disjressuc2  39118  elrefrels2  39305  refreleq  39308  elcnvrefrels2  39321  pmodN  40682  polvalN  40737  polatN  40763  trnsetN  40988  djavalN  41967  dihmeetbclemN  42136  dihmeetlem11N  42149  djhval  42230  lclkrlem2e  42343  lcfrlem23  42397  lcdlss2N  42452  elrfi  43483  elrfirn  43484  elrfirn2  43485  eldioph2lem1  43549  conrel2d  44448  ntrkbimka  44822  ntrk0kbimka  44823  isotone2  44833  ntrclskb  44853  ntrclsk3  44854  ntrclsk13  44855  clsneibex  44886  neicvgbex  44896  ismnushort  45069  relpfrlem  45720  inabs3  45834  disjiun2  45836  fresin2  45948  lptioo2  46405  lptioo1  46406  limsupvaluz  46480  cncfuni  46658  fourierdlem48  46926  fourierdlem49  46927  fourierdlem93  46971  qndenserrnbllem  47066  nnfoctbdjlem  47227  carageniuncllem1  47293  carageniuncllem2  47294  hoiqssbllem3  47396  smflimlem3  47545  smflim  47549  resinsnALT  49708  restclsseplem  49750