Theorem ineq2i 4116

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

This proof depends on syntax axioms:   = wceq 1569   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-in 4093

This theorem is used by:  in4  4132  inindir  4134  indif2  4228  difun1  4246  dfrab3ss  4270  undif1  4432  difdifdir  4449  dfif3  4499  dfif5  4501  disjpr2  4673  disjprsn  4674  disjtp2  4676  intunsn  4949  rint0  4950  uniin2  5036  riin0  5044  csbres  5977  res0  5978  resres  5987  resundi  5988  resindi  5990  inres  5992  resiun2  5995  resopab  6031  dffr3  6102  dfse2  6103  dminxp  6177  imainrect  6178  cnvrescnv  6193  resdmres  6239  resdifdi  6243  dfpo2  6305  snres0  6307  dfpred2  6320  predidm  6335  funimacnv  6629  fresaun  6761  fresaunres2  6762  tfrlem10  8406  sbthlem5  9121  infssuni  9346  dfsup2  9446  en3lplem2  9624  wemapwe  9708  epfrs  9742  r0weon  10101  infxpenlem  10102  kmlem11  10249  ackbij1lem1  10307  ackbij1lem2  10308  axdc3lem4  10541  canthwelem  10745  dmaddpi  10985  dmmulpi  10986  ssxr  11389  dmhashres  14495  fz1isolem  14616  f1oun2prg  15080  fsumiun  16000  sadeq  16654  bitsres  16655  smuval2  16664  smumul  16675  ressinbas  17435  lubdm  18535  glbdm  18548  sylow2a  19845  lsmmod2  19902  lsmdisj2r  19911  ablfac1eu  20301  pjdm  22025  ressmplbas2  22347  opsrtoslem1  22376  rintopn  23239  ordtrest2  23534  cmpsublem  23729  kgentopon  23869  hausdiag  23976  uzrest  24228  ufprim  24240  trust  24560  metnrmlem3  25193  clsocv  25583  ismbl  25859  unmbl  25870  volinun  25879  voliunlem1  25883  ovolioo  25901  itg2cnlem2  26095  ellimc2  26209  limcflf  26213  lhop1lem  26345  lgsquadlem3  27721  rplogsum  27866  noextend  28035  noextendseq  28036  noetasuplem2  28103  noetainflem2  28107  madeval2  28231  oniso  28669  bdayn0sf1o  28768  umgrislfupgrlem  29712  spthispth  30321  cyclnumvtx  30400  0pth  30728  1pthdlem2  30739  frgrncvvdeqlem3  30914  ex-in  31038  chdmj3i  32097  chdmj4i  32098  chjassi  32100  pjoml2i  32199  pjoml3i  32200  cmcmlem  32205  cmcm2i  32207  cmbr3i  32214  fh3i  32237  fh4i  32238  osumcor2i  32258  mayetes3i  32343  mdslmd3i  32946  mdexchi  32949  atabsi  33015  dmdbr5ati  33036  inin  33166  of0r  33327  dfprm3  34138  psrbasfsupp  34196  selvply1rhmlemb  34204  ordtrest2NEW  34608  hasheuni  34770  carsgclctunlem1  35002  eulerpartgbij  35057  fiblem  35083  j0ltalephlem  35961  cvmscld  36159  sate0  36301  msrid  36431  elrn3  36654  bj-inrab3  37969  poimirlem15  38693  mblfinlem2  38716  ftc1anclem6  38756  dmxrncnvep  39461  dmcnvepres  39462  dmuncnvepres  39463  dmxrnuncnvepres  39464  xrnres2  39498  redundss3  39784  refrelsredund4  39788  dfpetparts2  40044  dfpeters2  40046  pol0N  41106  readvrec2  43552  mapfzcons2  43870  diophrw  43910  conrel2d  44804  iunrelexp0  44842  hashnzfz  45444  wfaxpow  46126  disjinfi  46346  fourierdlem80  47335  sge0resplit  47555  sge0split  47558  caragenuncllem  47661  iscnrm3rlem1  50193