Theorem ineq2i 3546

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 3543	. 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 1364   i^i cin 3324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332

This theorem is referenced by:  in4  3563  inindir  3565  indif2  3590  difun1  3607  dfrab3ss  3625  undif1  3751  difdifdir  3763  dfif3  3800  dfif5  3802  intunsn  4164  rint0  4165  riin0  4241  csbres  5109  res0  5111  resres  5120  resundi  5121  resindi  5123  inres  5125  resiun2  5127  resopab  5150  dffr3  5198  dfse2  5199  dminxp  5275  imainrect  5276  resdmres  5326  funimacnv  5487  fresaun  5579  fresaunres2  5580  tfrlem10  6842  sbthlem5  7421  infssuni  7598  dfsup2  7688  dfsup2OLD  7689  dfsup3OLD  7690  en3lplem2  7817  wemapwe  7924  wemapweOLD  7925  epfrs  7947  r0weon  8175  infxpenlem  8176  kmlem11  8325  ackbij1lem1  8385  ackbij1lem2  8386  axdc3lem4  8618  canthwelem  8813  dmaddpi  9055  dmmulpi  9056  ssxr  9440  dmhashres  12108  fz1isolem  12210  f1oun2prg  12523  fsumiun  13280  sadeq  13664  bitsres  13665  smuval2  13674  smumul  13685  ressinbas  14230  lubdm  15145  glbdm  15158  sylow2a  16111  lsmmod2  16166  lsmdisj2r  16175  ablfac1eu  16564  ressmplbas2  17512  opsrtoslem1  17541  pjdm  18091  rintopn  18481  ordtrest2  18767  cmpsublem  18961  bwthOLD  18973  kgentopon  19070  hausdiag  19177  uzrest  19429  ufprim  19441  trust  19763  metnrmlem3  20396  clsocv  20721  ismbl  20968  unmbl  20978  volinun  20986  voliunlem1  20990  ovolioo  21008  itg2cnlem2  21199  ellimc2  21311  limcflf  21315  lhop1lem  21444  lgsquadlem3  22654  rplogsum  22735  0pth  23404  1pthonlem2  23424  ex-in  23567  chdmj3i  24821  chdmj4i  24822  chjassi  24824  pjoml2i  24923  pjoml3i  24924  cmcmlem  24929  cmcm2i  24931  cmbr3i  24938  fh3i  24961  fh4i  24962  osumcor2i  24982  mayetes3i  25068  mdslmd3i  25671  mdexchi  25674  atabsi  25740  dmdbr5ati  25761  inin  25831  ordtrest2NEW  26289  hasheuni  26470  eulerpartgbij  26685  fiblem  26711  cvmscld  27092  dfpo2  27494  elrn3  27502  dfpred2  27563  predidm  27578  wfrlem13  27665  mblfinlem2  28354  ftc1anclem6  28397  mapfzcons2  28980  diophrw  29022  frgrancvvdeqlem4  30551  pol0N  33275