Theorem ineq2i 4163

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

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 3898

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  in4  4179  inindir  4181  indif2  4227  difun1  4245  dfrab3ss  4269  undif1  4430  difdifdir  4447  dfif3  4497  dfif5  4499  disjpr2  4674  disjprsn  4675  disjtp2  4677  intunsn  4947  rint0  4948  uniin2  5034  riin0  5042  csbres  5975  res0  5976  resres  5985  resundi  5986  resindi  5988  inres  5990  resiun2  5993  resopab  6030  dffr3  6095  dfse2  6096  dminxp  6173  imainrect  6174  cnvrescnv  6189  resdmres  6228  resdifdi  6232  dfpo2  6294  snres0  6296  dfpred2  6309  predidm  6324  funimacnv  6615  fresaun  6747  fresaunres2  6748  tfrlem10  8377  sbthlem5  9092  infssuni  9316  dfsup2  9417  en3lplem2  9595  wemapwe  9679  epfrs  9713  r0weon  10018  infxpenlem  10019  kmlem11  10166  ackbij1lem1  10224  ackbij1lem2  10225  axdc3lem4  10458  canthwelem  10662  dmaddpi  10902  dmmulpi  10903  ssxr  11306  dmhashres  14408  fz1isolem  14529  f1oun2prg  14991  fsumiun  15911  sadeq  16565  bitsres  16566  smuval2  16575  smumul  16586  ressinbas  17340  lubdm  18440  glbdm  18453  sylow2a  19749  lsmmod2  19806  lsmdisj2r  19815  ablfac1eu  20205  pjdm  21923  ressmplbas2  22245  opsrtoslem1  22274  rintopn  23137  ordtrest2  23432  cmpsublem  23627  kgentopon  23767  hausdiag  23874  uzrest  24126  ufprim  24138  trust  24458  metnrmlem3  25091  clsocv  25481  ismbl  25757  unmbl  25768  volinun  25777  voliunlem1  25781  ovolioo  25799  itg2cnlem2  25993  ellimc2  26107  limcflf  26111  lhop1lem  26243  lgsquadlem3  27621  rplogsum  27766  noextend  27905  noextendseq  27906  noetasuplem2  27973  noetainflem2  27977  madeval2  28101  oniso  28539  bdayn0sf1o  28638  umgrislfupgrlem  29582  spthispth  30191  cyclnumvtx  30270  0pth  30598  1pthdlem2  30609  frgrncvvdeqlem3  30784  ex-in  30908  chdmj3i  31967  chdmj4i  31968  chjassi  31970  pjoml2i  32069  pjoml3i  32070  cmcmlem  32075  cmcm2i  32077  cmbr3i  32084  fh3i  32107  fh4i  32108  osumcor2i  32128  mayetes3i  32213  mdslmd3i  32816  mdexchi  32819  atabsi  32885  dmdbr5ati  32906  inin  32994  of0r  33155  dfprm3  33966  psrbasfsupp  34024  selvply1rhmlemb  34032  ordtrest2NEW  34436  hasheuni  34598  carsgclctunlem1  34831  eulerpartgbij  34886  fiblem  34912  cvmscld  35855  sate0  35997  msrid  36127  elrn3  36344  bj-inrab3  37676  poimirlem15  38387  mblfinlem2  38410  ftc1anclem6  38450  dmxrncnvep  39140  dmcnvepres  39141  dmuncnvepres  39142  dmxrnuncnvepres  39143  xrnres2  39177  redundss3  39463  refrelsredund4  39467  dfpetparts2  39723  dfpeters2  39725  pol0N  40785  readvrec2  43239  mapfzcons2  43567  diophrw  43607  conrel2d  44507  iunrelexp0  44545  hashnzfz  45147  wfaxpow  45823  disjinfi  46027  fourierdlem80  47017  sge0resplit  47237  sge0split  47240  caragenuncllem  47343  iscnrm3rlem1  49869