Theorem ineq2i 3499

Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)

Hypothesis

Ref	Expression
ineq1i.1	|- A = B

Assertion

Ref	Expression
ineq2i	|- ( C i^i A ) = ( C i^i B )

Proof of Theorem ineq2i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 |- A = B
2		ineq2 3496	. 2 |- ( A = B -> ( C i^i A ) = ( C i^i B ) )
3	1, 2	ax-mp 8	1 |- ( C i^i A ) = ( C i^i B )

Syntax hints:   = wceq 1649   i^i cin 3279

This theorem is referenced by:  in4  3517  inindir  3519  indif2  3544  difun1  3561  dfrab3ss  3579  undif1  3663  difdifdir  3675  dfif3  3709  dfif5  3711  intunsn  4049  rint0  4050  riin0  4124  res0  5109  resres  5118  resundi  5119  resindi  5121  inres  5123  resiun2  5125  resopab  5146  dffr3  5195  dfse2  5196  dminxp  5270  imainrect  5271  resdmres  5320  funimacnv  5484  fresaun  5573  fresaunres2  5574  tfrlem10  6607  sbthlem5  7180  dfsup2  7405  dfsup2OLD  7406  dfsup3OLD  7407  wemapwe  7610  epfrs  7623  en3lplem2  7627  r0weon  7850  infxpenlem  7851  kmlem11  7996  ackbij1lem1  8056  ackbij1lem2  8057  axdc3lem4  8289  canthwelem  8481  dmaddpi  8723  dmmulpi  8724  ssxr  9101  fz1isolem  11665  f1oun2prg  11819  fsumiun  12555  sadeq  12939  bitsres  12940  smuval2  12949  smumul  12960  ressinbas  13480  sylow2a  15208  lsmmod2  15263  lsmdisj2r  15272  ablfac1eu  15586  ressmplbas2  16473  opsrtoslem1  16499  pjdm  16889  rintopn  16937  ordtrest2  17222  cmpsublem  17416  kgentopon  17523  hausdiag  17630  uzrest  17882  ufprim  17894  trust  18212  metnrmlem3  18844  clsocv  19157  ismbl  19375  unmbl  19385  volinun  19393  voliunlem1  19397  ovolioo  19415  itg2cnlem2  19607  ellimc2  19717  limcflf  19721  lhop1lem  19850  lgsquadlem3  21093  rplogsum  21174  0pth  21523  1pthonlem2  21543  ex-in  21686  chdmj3i  22938  chdmj4i  22939  chjassi  22941  pjoml2i  23040  pjoml3i  23041  cmcmlem  23046  cmcm2i  23048  cmbr3i  23055  fh3i  23078  fh4i  23079  osumcor2i  23099  mayetes3i  23185  mdslmd3i  23788  mdexchi  23791  atabsi  23857  dmdbr5ati  23878  inin  23949  dmhashres  24110  hasheuni  24428  cvmscld  24913  dfpo2  25326  elrn3  25334  dfpred2  25389  predidm  25402  wfrlem13  25482  mblfinlem  26143  mapfzcons2  26665  diophrw  26707  frgrancvvdeqlem4  28136  pol0N  30391

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287