Theorem ineq2i 3661

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 3658	. 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 1437   i^i cin 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443

This theorem is referenced by:  in4  3678  inindir  3680  indif2  3716  difun1  3733  dfrab3ss  3751  undif1  3872  difdifdir  3885  dfif3  3925  dfif5  3927  intunsn  4295  rint0  4296  riin0  4373  csbres  5127  res0  5128  resres  5136  resundi  5137  resindi  5139  inres  5141  resiun2  5143  resopab  5170  dffr3  5220  dfse2  5221  dminxp  5296  imainrect  5297  resdmres  5345  dfpred2  5408  predidm  5421  funimacnv  5673  fresaun  5771  fresaunres2  5772  wfrlem13  7059  tfrlem10  7116  sbthlem5  7695  infssuni  7874  dfsup2  7967  en3lplem2  8129  wemapwe  8210  epfrs  8223  r0weon  8451  infxpenlem  8452  kmlem11  8597  ackbij1lem1  8657  ackbij1lem2  8658  axdc3lem4  8890  canthwelem  9082  dmaddpi  9322  dmmulpi  9323  ssxr  9710  dmhashres  12530  fz1isolem  12628  f1oun2prg  13002  fsumiun  13880  sadeq  14445  bitsres  14446  smuval2  14455  smumul  14466  ressinbas  15184  lubdm  16224  glbdm  16237  sylow2a  17270  lsmmod2  17325  lsmdisj2r  17334  ablfac1eu  17705  ressmplbas2  18678  opsrtoslem1  18706  pjdm  19268  rintopn  19937  ordtrest2  20218  cmpsublem  20412  kgentopon  20551  hausdiag  20658  uzrest  20910  ufprim  20922  trust  21242  metnrmlem3  21876  metnrmlem3OLD  21891  clsocv  22219  ismbl  22478  unmbl  22489  volinun  22497  voliunlem1  22501  ovolioo  22519  itg2cnlem2  22718  ellimc2  22830  limcflf  22834  lhop1lem  22963  lgsquadlem3  24282  rplogsum  24363  0pth  25298  1pthonlem2  25318  frgrancvvdeqlem4  25759  ex-in  25873  chdmj3i  27134  chdmj4i  27135  chjassi  27137  pjoml2i  27236  pjoml3i  27237  cmcmlem  27242  cmcm2i  27244  cmbr3i  27251  fh3i  27274  fh4i  27275  osumcor2i  27295  mayetes3i  27380  mdslmd3i  27983  mdexchi  27986  atabsi  28052  dmdbr5ati  28073  inin  28148  uniin2  28167  ordtrest2NEW  28737  hasheuni  28914  carsgclctunlem1  29157  eulerpartgbij  29213  fiblem  29239  cvmscld  30004  msrid  30191  dfpo2  30402  elrn3  30410  bj-inrab3  31501  poimirlem15  31919  mblfinlem2  31942  ftc1anclem6  31986  pol0N  33443  mapfzcons2  35530  diophrw  35570  conrel2d  36226  iunrelexp0  36264  hashnzfz  36639  disjinfi  37429  fourierdlem80  37990  sge0resplit  38156  sge0split  38159  caragenuncllem  38241