Theorem ineq2i 4171

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

Syntax hints:   = wceq 1542   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910

This theorem is referenced by:  in4  4188  inindir  4190  indif2  4235  difun1  4253  dfrab3ss  4277  undif1  4430  difdifdir  4446  dfif3  4496  dfif5  4498  disjpr2  4672  disjprsn  4673  disjtp2  4675  intunsn  4944  rint0  4945  riin0  5039  csbres  5949  res0  5950  resres  5959  resundi  5960  resindi  5962  inres  5964  resiun2  5967  resopab  6001  dffr3  6066  dfse2  6067  dminxp  6146  imainrect  6147  cnvrescnv  6161  resdmres  6198  resdifdi  6202  dfpo2  6262  snres0  6264  dfpred2  6277  predidm  6292  funimacnv  6581  fresaun  6713  fresaunres2  6714  tfrlem10  8328  sbthlem5  9031  infssuni  9258  dfsup2  9359  en3lplem2  9534  wemapwe  9618  epfrs  9652  r0weon  9934  infxpenlem  9935  kmlem11  10083  ackbij1lem1  10141  ackbij1lem2  10142  axdc3lem4  10375  canthwelem  10573  dmaddpi  10813  dmmulpi  10814  ssxr  11214  dmhashres  14276  fz1isolem  14396  f1oun2prg  14852  fsumiun  15756  sadeq  16411  bitsres  16412  smuval2  16421  smumul  16432  ressinbas  17184  lubdm  18284  glbdm  18297  sylow2a  19560  lsmmod2  19617  lsmdisj2r  19626  ablfac1eu  20016  pjdm  21674  ressmplbas2  21994  opsrtoslem1  22022  rintopn  22865  ordtrest2  23160  cmpsublem  23355  kgentopon  23494  hausdiag  23601  uzrest  23853  ufprim  23865  trust  24185  metnrmlem3  24818  clsocv  25218  ismbl  25495  unmbl  25506  volinun  25515  voliunlem1  25519  ovolioo  25537  itg2cnlem2  25731  ellimc2  25846  limcflf  25850  lhop1lem  25986  lgsquadlem3  27361  rplogsum  27506  noextend  27646  noextendseq  27647  noetasuplem2  27714  noetainflem2  27718  madeval2  27841  oniso  28279  bdayn0sf1o  28378  umgrislfupgrlem  29207  spthispth  29809  cyclnumvtx  29885  0pth  30212  1pthdlem2  30223  frgrncvvdeqlem3  30388  ex-in  30512  chdmj3i  31571  chdmj4i  31572  chjassi  31574  pjoml2i  31673  pjoml3i  31674  cmcmlem  31679  cmcm2i  31681  cmbr3i  31688  fh3i  31711  fh4i  31712  osumcor2i  31732  mayetes3i  31817  mdslmd3i  32420  mdexchi  32423  atabsi  32489  dmdbr5ati  32510  inin  32603  uniin2  32639  of0r  32769  dfprm3  33646  psrbasfsupp  33705  ordtrest2NEW  34101  hasheuni  34263  carsgclctunlem1  34495  eulerpartgbij  34550  fiblem  34576  cvmscld  35489  sate0  35631  msrid  35761  elrn3  35978  bj-inrab3  37177  poimirlem15  37886  mblfinlem2  37909  ftc1anclem6  37949  dmxrncnvep  38640  dmcnvepres  38641  dmuncnvepres  38642  dmxrnuncnvepres  38643  xrnres2  38677  redundss3  38963  refrelsredund4  38967  dfpetparts2  39223  dfpeters2  39225  pol0N  40285  readvrec2  42731  mapfzcons2  43076  diophrw  43116  conrel2d  44020  iunrelexp0  44058  hashnzfz  44676  wfaxpow  45353  disjinfi  45551  fourierdlem80  46544  sge0resplit  46764  sge0split  46767  caragenuncllem  46870  iscnrm3rlem1  49299