Theorem ineq2i 4224

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

Syntax hints:   = wceq 1536   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969

This theorem is referenced by:  in4  4241  inindir  4243  indif2  4286  difun1  4304  dfrab3ss  4328  undif1  4481  difdifdir  4497  dfif3  4544  dfif5  4546  disjpr2  4717  disjprsn  4718  disjtp2  4720  intunsn  4991  rint0  4992  riin0  5086  csbres  6002  res0  6003  resres  6012  resundi  6013  resindi  6015  inres  6017  resiun2  6020  resopab  6053  dffr3  6119  dfse2  6120  dminxp  6201  imainrect  6202  cnvrescnv  6216  resdmres  6253  resdifdi  6257  dfpo2  6317  snres0  6319  dfpred2  6332  predidm  6348  funimacnv  6648  fresaun  6779  fresaunres2  6780  wfrlem13OLD  8359  tfrlem10  8425  sbthlem5  9125  infssuni  9383  dfsup2  9481  en3lplem2  9650  wemapwe  9734  epfrs  9768  r0weon  10049  infxpenlem  10050  kmlem11  10198  ackbij1lem1  10256  ackbij1lem2  10257  axdc3lem4  10490  canthwelem  10687  dmaddpi  10927  dmmulpi  10928  ssxr  11327  dmhashres  14376  fz1isolem  14496  f1oun2prg  14952  fsumiun  15853  sadeq  16505  bitsres  16506  smuval2  16515  smumul  16526  ressinbas  17290  lubdm  18408  glbdm  18421  sylow2a  19651  lsmmod2  19708  lsmdisj2r  19717  ablfac1eu  20107  pjdm  21744  ressmplbas2  22062  opsrtoslem1  22096  rintopn  22930  ordtrest2  23227  cmpsublem  23422  kgentopon  23561  hausdiag  23668  uzrest  23920  ufprim  23932  trust  24253  metnrmlem3  24896  clsocv  25297  ismbl  25574  unmbl  25585  volinun  25594  voliunlem1  25598  ovolioo  25616  itg2cnlem2  25811  ellimc2  25926  limcflf  25930  lhop1lem  26066  lgsquadlem3  27440  rplogsum  27585  noextend  27725  noextendseq  27726  noetasuplem2  27793  noetainflem2  27797  madeval2  27906  umgrislfupgrlem  29153  spthispth  29758  0pth  30153  1pthdlem2  30164  frgrncvvdeqlem3  30329  ex-in  30453  chdmj3i  31511  chdmj4i  31512  chjassi  31514  pjoml2i  31613  pjoml3i  31614  cmcmlem  31619  cmcm2i  31621  cmbr3i  31628  fh3i  31651  fh4i  31652  osumcor2i  31672  mayetes3i  31757  mdslmd3i  32360  mdexchi  32363  atabsi  32429  dmdbr5ati  32450  inin  32543  uniin2  32572  of0r  32694  dfprm3  33560  ordtrest2NEW  33883  hasheuni  34065  carsgclctunlem1  34298  eulerpartgbij  34353  fiblem  34379  cvmscld  35257  sate0  35399  msrid  35529  elrn3  35741  bj-inrab3  36911  poimirlem15  37621  mblfinlem2  37644  ftc1anclem6  37684  xrnres2  38384  redundss3  38609  refrelsredund4  38613  pol0N  39891  readvrec2  42369  mapfzcons2  42706  diophrw  42746  conrel2d  43653  iunrelexp0  43691  hashnzfz  44315  disjinfi  45134  fourierdlem80  46141  sge0resplit  46361  sge0split  46364  caragenuncllem  46467  iscnrm3rlem1  48736