Theorem ineq2i 4208

Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)

Hypothesis

Ref	Expression
ineq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
ineq2i	⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)

Proof of Theorem ineq2i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		ineq2 4205	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)

Syntax hints:   = wceq 1539   ∩ cin 3946

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-in 3954

This theorem is referenced by:  in4  4224  inindir  4226  indif2  4269  difun1  4288  dfrab3ss  4311  undif1  4474  difdifdir  4490  dfif3  4541  dfif5  4543  disjpr2  4716  disjprsn  4717  disjtp2  4719  intunsn  4992  rint0  4993  riin0  5084  csbres  5983  res0  5984  resres  5993  resundi  5994  resindi  5996  inres  5998  resiun2  6001  resopab  6033  dffr3  6097  dfse2  6098  dminxp  6178  imainrect  6179  cnvrescnv  6193  resdmres  6230  resdifdi  6234  dfpo2  6294  snres0  6296  dfpred2  6309  predidm  6326  funimacnv  6628  fresaun  6761  fresaunres2  6762  wfrlem13OLD  8323  tfrlem10  8389  sbthlem5  9089  infssuni  9345  dfsup2  9441  en3lplem2  9610  wemapwe  9694  epfrs  9728  r0weon  10009  infxpenlem  10010  kmlem11  10157  ackbij1lem1  10217  ackbij1lem2  10218  axdc3lem4  10450  canthwelem  10647  dmaddpi  10887  dmmulpi  10888  ssxr  11287  dmhashres  14305  fz1isolem  14426  f1oun2prg  14872  fsumiun  15771  sadeq  16417  bitsres  16418  smuval2  16427  smumul  16438  ressinbas  17194  lubdm  18308  glbdm  18321  sylow2a  19528  lsmmod2  19585  lsmdisj2r  19594  ablfac1eu  19984  pjdm  21481  ressmplbas2  21801  opsrtoslem1  21835  rintopn  22631  ordtrest2  22928  cmpsublem  23123  kgentopon  23262  hausdiag  23369  uzrest  23621  ufprim  23633  trust  23954  metnrmlem3  24597  clsocv  24998  ismbl  25275  unmbl  25286  volinun  25295  voliunlem1  25299  ovolioo  25317  itg2cnlem2  25512  ellimc2  25626  limcflf  25630  lhop1lem  25765  lgsquadlem3  27121  rplogsum  27266  noextend  27405  noextendseq  27406  noetasuplem2  27473  noetainflem2  27477  madeval2  27585  umgrislfupgrlem  28649  spthispth  29250  0pth  29645  1pthdlem2  29656  frgrncvvdeqlem3  29821  ex-in  29945  chdmj3i  31003  chdmj4i  31004  chjassi  31006  pjoml2i  31105  pjoml3i  31106  cmcmlem  31111  cmcm2i  31113  cmbr3i  31120  fh3i  31143  fh4i  31144  osumcor2i  31164  mayetes3i  31249  mdslmd3i  31852  mdexchi  31855  atabsi  31921  dmdbr5ati  31942  inin  32020  uniin2  32051  ordtrest2NEW  33201  hasheuni  33381  carsgclctunlem1  33614  eulerpartgbij  33669  fiblem  33695  cvmscld  34562  sate0  34704  msrid  34834  elrn3  35036  bj-inrab3  36112  poimirlem15  36806  mblfinlem2  36829  ftc1anclem6  36869  xrnres2  37576  redundss3  37801  refrelsredund4  37805  pol0N  39083  mapfzcons2  41759  diophrw  41799  conrel2d  42717  iunrelexp0  42755  hashnzfz  43381  disjinfi  44189  fourierdlem80  45200  sge0resplit  45420  sge0split  45423  caragenuncllem  45526  iscnrm3rlem1  47660