MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineq2i Unicode version

Theorem ineq2i 3380
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
StepHypRef Expression
1 ineq1i.1 . 2  |-  A  =  B
2 ineq2 3377 . 2  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
31, 2ax-mp 8 1  |-  ( C  i^i  A )  =  ( C  i^i  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1632    i^i cin 3164
This theorem is referenced by:  in4  3398  inindir  3400  indif2  3425  difun1  3441  dfrab3ss  3459  undif1  3542  difdifdir  3554  dfif3  3588  dfif5  3590  intunsn  3917  rint0  3918  riin0  3991  resiundiOLD  4761  res0  4975  resres  4984  resundi  4985  resindi  4987  inres  4989  resiun2  4991  resopab  5012  dffr3  5061  dfse2  5062  dminxp  5134  imainrect  5135  resdmres  5180  funimacnv  5340  fresaun  5428  fresaunres2  5429  tfrlem10  6419  sbthlem5  6991  dfsup2  7211  dfsup2OLD  7212  dfsup3OLD  7213  wemapwe  7416  epfrs  7429  en3lplem2  7433  r0weon  7656  infxpenlem  7657  kmlem11  7802  ackbij1lem1  7862  ackbij1lem2  7863  axdc3lem4  8095  canthwelem  8288  dmaddpi  8530  dmmulpi  8531  ssxr  8908  fz1isolem  11415  fsumiun  12295  sadeq  12679  bitsres  12680  smuval2  12689  smumul  12700  ressinbas  13220  sylow2a  14946  lsmmod2  15001  lsmdisj2r  15010  ablfac1eu  15324  ressmplbas2  16215  opsrtoslem1  16241  pjdm  16623  rintopn  16671  ordtrest2  16950  cmpsublem  17142  kgentopon  17249  hausdiag  17355  uzrest  17608  ufprim  17620  metnrmlem3  18381  clsocv  18693  ismbl  18901  unmbl  18911  volinun  18919  voliunlem1  18923  ovolioo  18941  itg2cnlem2  19133  ellimc2  19243  limcflf  19247  lhop1lem  19376  lgsquadlem3  20611  rplogsum  20692  ex-in  20828  chdmj3i  22078  chdmj4i  22079  chjassi  22081  pjoml2i  22180  pjoml3i  22181  cmcmlem  22186  cmcm2i  22188  cmbr3i  22195  fh3i  22218  fh4i  22219  osumcor2i  22239  mayetes3i  22325  mdslmd3i  22928  mdexchi  22931  atabsi  22997  dmdbr5ati  23018  inin  23183  dmhashres  23190  hasheuni  23468  cvmscld  23819  dfpo2  24183  elrn3  24191  dfpred2  24246  predidm  24259  wfrlem13  24339  isunscov  25177  inabs2  25241  empos  25345  inposet  25381  dispos  25390  islimrs4  25685  bwt2  25695  hdrmp  25809  mapfzcons2  26899  diophrw  26941  f1oun2prg  28187  0pth  28356  pol0N  30720
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator