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

Theorem ineq2i 3484
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 3481 . 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 1649    i^i cin 3264
This theorem is referenced by:  in4  3502  inindir  3504  indif2  3529  difun1  3546  dfrab3ss  3564  undif1  3648  difdifdir  3660  dfif3  3694  dfif5  3696  intunsn  4033  rint0  4034  riin0  4107  res0  5092  resres  5101  resundi  5102  resindi  5104  inres  5106  resiun2  5108  resopab  5129  dffr3  5178  dfse2  5179  dminxp  5253  imainrect  5254  resdmres  5303  funimacnv  5467  fresaun  5556  fresaunres2  5557  tfrlem10  6586  sbthlem5  7159  dfsup2  7384  dfsup2OLD  7385  dfsup3OLD  7386  wemapwe  7589  epfrs  7602  en3lplem2  7606  r0weon  7829  infxpenlem  7830  kmlem11  7975  ackbij1lem1  8035  ackbij1lem2  8036  axdc3lem4  8268  canthwelem  8460  dmaddpi  8702  dmmulpi  8703  ssxr  9080  fz1isolem  11639  f1oun2prg  11793  fsumiun  12529  sadeq  12913  bitsres  12914  smuval2  12923  smumul  12934  ressinbas  13454  sylow2a  15182  lsmmod2  15237  lsmdisj2r  15246  ablfac1eu  15560  ressmplbas2  16447  opsrtoslem1  16473  pjdm  16859  rintopn  16907  ordtrest2  17192  cmpsublem  17386  kgentopon  17493  hausdiag  17600  uzrest  17852  ufprim  17864  trust  18182  metnrmlem3  18764  clsocv  19077  ismbl  19291  unmbl  19301  volinun  19309  voliunlem1  19313  ovolioo  19331  itg2cnlem2  19523  ellimc2  19633  limcflf  19637  lhop1lem  19766  lgsquadlem3  21009  rplogsum  21090  0pth  21426  1pthonlem2  21440  ex-in  21583  chdmj3i  22835  chdmj4i  22836  chjassi  22838  pjoml2i  22937  pjoml3i  22938  cmcmlem  22943  cmcm2i  22945  cmbr3i  22952  fh3i  22975  fh4i  22976  osumcor2i  22996  mayetes3i  23082  mdslmd3i  23685  mdexchi  23688  atabsi  23754  dmdbr5ati  23775  inin  23842  dmhashres  23997  hasheuni  24273  cvmscld  24741  dfpo2  25138  elrn3  25146  dfpred2  25201  predidm  25214  wfrlem13  25294  mapfzcons2  26468  diophrw  26510  frgrancvvdeqlem4  27787  pol0N  30025
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-in 3272
  Copyright terms: Public domain W3C validator