Theorem ineq2i 4170

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 4167	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)

This proof depends on syntax axioms:   = 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:  in4  4186  inindir  4188  indif2  4234  difun1  4252  dfrab3ss  4276  undif1  4437  difdifdir  4454  dfif3  4504  dfif5  4506  disjpr2  4681  disjprsn  4682  disjtp2  4684  intunsn  4954  rint0  4955  uniin2  5042  riin0  5050  csbres  5983  res0  5984  resres  5993  resundi  5994  resindi  5996  inres  5998  resiun2  6001  resopab  6038  dffr3  6103  dfse2  6104  dminxp  6180  imainrect  6181  cnvrescnv  6196  resdmres  6235  resdifdi  6239  dfpo2  6301  snres0  6303  dfpred2  6316  predidm  6331  funimacnv  6621  fresaun  6753  fresaunres2  6754  tfrlem10  8380  sbthlem5  9086  infssuni  9310  dfsup2  9411  en3lplem2  9589  wemapwe  9673  epfrs  9707  r0weon  10012  infxpenlem  10013  kmlem11  10160  ackbij1lem1  10218  ackbij1lem2  10219  axdc3lem4  10452  canthwelem  10652  dmaddpi  10892  dmmulpi  10893  ssxr  11296  dmhashres  14397  fz1isolem  14518  f1oun2prg  14980  fsumiun  15898  sadeq  16554  bitsres  16555  smuval2  16564  smumul  16575  ressinbas  17329  lubdm  18429  glbdm  18442  sylow2a  19735  lsmmod2  19792  lsmdisj2r  19801  ablfac1eu  20191  pjdm  21909  ressmplbas2  22229  opsrtoslem1  22258  rintopn  23118  ordtrest2  23413  cmpsublem  23608  kgentopon  23748  hausdiag  23855  uzrest  24107  ufprim  24119  trust  24439  metnrmlem3  25072  clsocv  25462  ismbl  25738  unmbl  25749  volinun  25758  voliunlem1  25762  ovolioo  25780  itg2cnlem2  25974  ellimc2  26089  limcflf  26093  lhop1lem  26225  lgsquadlem3  27599  rplogsum  27744  noextend  27883  noextendseq  27884  noetasuplem2  27951  noetainflem2  27955  madeval2  28079  oniso  28517  bdayn0sf1o  28616  umgrislfupgrlem  29529  spthispth  30138  cyclnumvtx  30217  0pth  30545  1pthdlem2  30556  frgrncvvdeqlem3  30725  ex-in  30849  chdmj3i  31908  chdmj4i  31909  chjassi  31911  pjoml2i  32010  pjoml3i  32011  cmcmlem  32016  cmcm2i  32018  cmbr3i  32025  fh3i  32048  fh4i  32049  osumcor2i  32069  mayetes3i  32154  mdslmd3i  32757  mdexchi  32760  atabsi  32826  dmdbr5ati  32847  inin  32935  of0r  33097  dfprm3  33909  psrbasfsupp  33967  selvply1rhmlemb  33975  ordtrest2NEW  34379  hasheuni  34541  carsgclctunlem1  34774  eulerpartgbij  34829  fiblem  34855  cvmscld  35804  sate0  35946  msrid  36076  elrn3  36293  bj-inrab3  37624  poimirlem15  38345  mblfinlem2  38368  ftc1anclem6  38408  dmxrncnvep  39098  dmcnvepres  39099  dmuncnvepres  39100  dmxrnuncnvepres  39101  xrnres2  39135  redundss3  39421  refrelsredund4  39425  dfpetparts2  39681  dfpeters2  39683  pol0N  40743  readvrec2  43182  mapfzcons2  43510  diophrw  43550  conrel2d  44450  iunrelexp0  44488  hashnzfz  45090  wfaxpow  45766  disjinfi  45970  fourierdlem80  46960  sge0resplit  47180  sge0split  47183  caragenuncllem  47286  iscnrm3rlem1  49777