Theorem ineq2i 3697

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 3694	. 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 1379   i^i cin 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483

This theorem is referenced by:  in4  3714  inindir  3716  indif2  3741  difun1  3758  dfrab3ss  3776  undif1  3902  difdifdir  3914  dfif3  3953  dfif5  3955  intunsn  4321  rint0  4322  riin0  4399  csbres  5274  res0  5276  resres  5284  resundi  5285  resindi  5287  inres  5289  resiun2  5291  resopab  5318  dffr3  5367  dfse2  5368  dminxp  5445  imainrect  5446  resdmres  5496  funimacnv  5658  fresaun  5754  fresaunres2  5755  tfrlem10  7053  sbthlem5  7628  infssuni  7807  dfsup2  7898  dfsup2OLD  7899  dfsup3OLD  7900  en3lplem2  8028  wemapwe  8135  wemapweOLD  8136  epfrs  8158  r0weon  8386  infxpenlem  8387  kmlem11  8536  ackbij1lem1  8596  ackbij1lem2  8597  axdc3lem4  8829  canthwelem  9024  dmaddpi  9264  dmmulpi  9265  ssxr  9650  dmhashres  12378  fz1isolem  12472  f1oun2prg  12824  fsumiun  13594  sadeq  13977  bitsres  13978  smuval2  13987  smumul  13998  ressinbas  14547  lubdm  15462  glbdm  15475  sylow2a  16435  lsmmod2  16490  lsmdisj2r  16499  ablfac1eu  16914  ressmplbas2  17888  opsrtoslem1  17919  pjdm  18505  rintopn  19185  ordtrest2  19471  cmpsublem  19665  bwthOLD  19677  kgentopon  19774  hausdiag  19881  uzrest  20133  ufprim  20145  trust  20467  metnrmlem3  21100  clsocv  21425  ismbl  21672  unmbl  21683  volinun  21691  voliunlem1  21695  ovolioo  21713  itg2cnlem2  21904  ellimc2  22016  limcflf  22020  lhop1lem  22149  lgsquadlem3  23359  rplogsum  23440  0pth  24248  1pthonlem2  24268  frgrancvvdeqlem4  24710  ex-in  24823  chdmj3i  26077  chdmj4i  26078  chjassi  26080  pjoml2i  26179  pjoml3i  26180  cmcmlem  26185  cmcm2i  26187  cmbr3i  26194  fh3i  26217  fh4i  26218  osumcor2i  26238  mayetes3i  26324  mdslmd3i  26927  mdexchi  26930  atabsi  26996  dmdbr5ati  27017  inin  27087  ordtrest2NEW  27541  hasheuni  27731  eulerpartgbij  27951  fiblem  27977  cvmscld  28358  dfpo2  28761  elrn3  28769  dfpred2  28830  predidm  28845  wfrlem13  28932  mblfinlem2  29629  ftc1anclem6  29672  mapfzcons2  30255  diophrw  30296  hashnzfz  30825  fourierdlem80  31487  pol0N  34705  conrel2d  36782