Theorem ineq2i 3564

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 3561	. 2 |- ( A = B -> ( C i^i A ) = ( C i^i B ) )
3	1, 2	ax-mp 5	1 |- ( C i^i A ) = ( C i^i B )

Syntax hints:   = wceq 1369   i^i cin 3342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2989  df-in 3350

This theorem is referenced by:  in4  3581  inindir  3583  indif2  3608  difun1  3625  dfrab3ss  3643  undif1  3769  difdifdir  3781  dfif3  3818  dfif5  3820  intunsn  4182  rint0  4183  riin0  4259  csbres  5128  res0  5130  resres  5138  resundi  5139  resindi  5141  inres  5143  resiun2  5145  resopab  5168  dffr3  5216  dfse2  5217  dminxp  5293  imainrect  5294  resdmres  5344  funimacnv  5505  fresaun  5597  fresaunres2  5598  tfrlem10  6861  sbthlem5  7440  infssuni  7617  dfsup2  7707  dfsup2OLD  7708  dfsup3OLD  7709  en3lplem2  7836  wemapwe  7943  wemapweOLD  7944  epfrs  7966  r0weon  8194  infxpenlem  8195  kmlem11  8344  ackbij1lem1  8404  ackbij1lem2  8405  axdc3lem4  8637  canthwelem  8832  dmaddpi  9074  dmmulpi  9075  ssxr  9459  dmhashres  12127  fz1isolem  12229  f1oun2prg  12542  fsumiun  13299  sadeq  13683  bitsres  13684  smuval2  13693  smumul  13704  ressinbas  14249  lubdm  15164  glbdm  15177  sylow2a  16133  lsmmod2  16188  lsmdisj2r  16197  ablfac1eu  16589  ressmplbas2  17549  opsrtoslem1  17580  pjdm  18147  rintopn  18537  ordtrest2  18823  cmpsublem  19017  bwthOLD  19029  kgentopon  19126  hausdiag  19233  uzrest  19485  ufprim  19497  trust  19819  metnrmlem3  20452  clsocv  20777  ismbl  21024  unmbl  21034  volinun  21042  voliunlem1  21046  ovolioo  21064  itg2cnlem2  21255  ellimc2  21367  limcflf  21371  lhop1lem  21500  lgsquadlem3  22710  rplogsum  22791  0pth  23484  1pthonlem2  23504  ex-in  23647  chdmj3i  24901  chdmj4i  24902  chjassi  24904  pjoml2i  25003  pjoml3i  25004  cmcmlem  25009  cmcm2i  25011  cmbr3i  25018  fh3i  25041  fh4i  25042  osumcor2i  25062  mayetes3i  25148  mdslmd3i  25751  mdexchi  25754  atabsi  25820  dmdbr5ati  25841  inin  25911  ordtrest2NEW  26368  hasheuni  26549  eulerpartgbij  26770  fiblem  26796  cvmscld  27177  dfpo2  27580  elrn3  27588  dfpred2  27649  predidm  27664  wfrlem13  27751  mblfinlem2  28448  ftc1anclem6  28491  mapfzcons2  29074  diophrw  29116  frgrancvvdeqlem4  30645  pol0N  33572