Theorem ineq2i 4169

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

Syntax hints:   = wceq 1560   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3911

This theorem is referenced by:  in4  4185  inindir  4187  indif2  4233  difun1  4251  dfrab3ss  4275  undif1  4430  difdifdir  4445  dfif3  4495  dfif5  4497  disjpr2  4672  disjprsn  4673  disjtp2  4675  intunsn  4945  rint0  4946  riin0  5039  csbres  5968  res0  5969  resres  5978  resundi  5979  resindi  5981  inres  5983  resiun2  5986  resopab  6023  dffr3  6088  dfse2  6089  dminxp  6166  imainrect  6167  cnvrescnv  6182  resdmres  6219  resdifdi  6223  dfpo2  6283  snres0  6285  dfpred2  6298  predidm  6313  funimacnv  6602  fresaun  6735  fresaunres2  6736  tfrlem10  8358  sbthlem5  9063  infssuni  9289  dfsup2  9390  en3lplem2  9568  wemapwe  9652  epfrs  9686  r0weon  9968  infxpenlem  9969  kmlem11  10117  ackbij1lem1  10175  ackbij1lem2  10176  axdc3lem4  10410  canthwelem  10608  dmaddpi  10848  dmmulpi  10849  ssxr  11252  dmhashres  14354  fz1isolem  14474  f1oun2prg  14930  fsumiun  15849  sadeq  16506  bitsres  16507  smuval2  16516  smumul  16527  ressinbas  17281  lubdm  18381  glbdm  18394  sylow2a  19659  lsmmod2  19716  lsmdisj2r  19725  ablfac1eu  20115  pjdm  21759  ressmplbas2  22079  opsrtoslem1  22108  rintopn  22969  ordtrest2  23264  cmpsublem  23459  kgentopon  23598  hausdiag  23705  uzrest  23957  ufprim  23969  trust  24289  metnrmlem3  24922  clsocv  25312  ismbl  25588  unmbl  25599  volinun  25608  voliunlem1  25612  ovolioo  25630  itg2cnlem2  25824  ellimc2  25939  limcflf  25943  lhop1lem  26075  lgsquadlem3  27446  rplogsum  27591  noextend  27730  noextendseq  27731  noetasuplem2  27798  noetainflem2  27802  madeval2  27926  oniso  28364  bdayn0sf1o  28463  umgrislfupgrlem  29323  spthispth  29924  cyclnumvtx  30000  0pth  30327  1pthdlem2  30338  frgrncvvdeqlem3  30503  ex-in  30627  chdmj3i  31686  chdmj4i  31687  chjassi  31689  pjoml2i  31788  pjoml3i  31789  cmcmlem  31794  cmcm2i  31796  cmbr3i  31803  fh3i  31826  fh4i  31827  osumcor2i  31847  mayetes3i  31932  mdslmd3i  32535  mdexchi  32538  atabsi  32604  dmdbr5ati  32625  inin  32715  uniin2  32752  of0r  32881  dfprm3  33749  psrbasfsupp  33808  selvply1rhmlemb  33816  ordtrest2NEW  34220  hasheuni  34382  carsgclctunlem1  34614  eulerpartgbij  34669  fiblem  34695  cvmscld  35623  sate0  35765  msrid  35895  elrn3  36112  bj-inrab3  37414  poimirlem15  38134  mblfinlem2  38157  ftc1anclem6  38197  dmxrncnvep  38888  dmcnvepres  38889  dmuncnvepres  38890  dmxrnuncnvepres  38891  xrnres2  38925  redundss3  39211  refrelsredund4  39215  dfpetparts2  39471  dfpeters2  39473  pol0N  40533  readvrec2  42970  mapfzcons2  43300  diophrw  43340  conrel2d  44240  iunrelexp0  44278  hashnzfz  44896  wfaxpow  45573  disjinfi  45770  fourierdlem80  46760  sge0resplit  46980  sge0split  46983  caragenuncllem  47086  iscnrm3rlem1  49561