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

Theorem ineq2i 3507
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 3504 . 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 3287
This theorem is referenced by:  in4  3525  inindir  3527  indif2  3552  difun1  3569  dfrab3ss  3587  undif1  3671  difdifdir  3683  dfif3  3717  dfif5  3719  intunsn  4057  rint0  4058  riin0  4132  res0  5117  resres  5126  resundi  5127  resindi  5129  inres  5131  resiun2  5133  resopab  5154  dffr3  5203  dfse2  5204  dminxp  5278  imainrect  5279  resdmres  5328  funimacnv  5492  fresaun  5581  fresaunres2  5582  tfrlem10  6615  sbthlem5  7188  dfsup2  7413  dfsup2OLD  7414  dfsup3OLD  7415  wemapwe  7618  epfrs  7631  en3lplem2  7635  r0weon  7858  infxpenlem  7859  kmlem11  8004  ackbij1lem1  8064  ackbij1lem2  8065  axdc3lem4  8297  canthwelem  8489  dmaddpi  8731  dmmulpi  8732  ssxr  9109  fz1isolem  11673  f1oun2prg  11827  fsumiun  12563  sadeq  12947  bitsres  12948  smuval2  12957  smumul  12968  ressinbas  13488  sylow2a  15216  lsmmod2  15271  lsmdisj2r  15280  ablfac1eu  15594  ressmplbas2  16481  opsrtoslem1  16507  pjdm  16897  rintopn  16945  ordtrest2  17230  cmpsublem  17424  kgentopon  17531  hausdiag  17638  uzrest  17890  ufprim  17902  trust  18220  metnrmlem3  18852  clsocv  19165  ismbl  19383  unmbl  19393  volinun  19401  voliunlem1  19405  ovolioo  19423  itg2cnlem2  19615  ellimc2  19725  limcflf  19729  lhop1lem  19858  lgsquadlem3  21101  rplogsum  21182  0pth  21531  1pthonlem2  21551  ex-in  21694  chdmj3i  22946  chdmj4i  22947  chjassi  22949  pjoml2i  23048  pjoml3i  23049  cmcmlem  23054  cmcm2i  23056  cmbr3i  23063  fh3i  23086  fh4i  23087  osumcor2i  23107  mayetes3i  23193  mdslmd3i  23796  mdexchi  23799  atabsi  23865  dmdbr5ati  23886  inin  23957  dmhashres  24118  hasheuni  24436  cvmscld  24921  dfpo2  25334  elrn3  25342  dfpred2  25397  predidm  25410  wfrlem13  25490  mblfinlem  26151  mapfzcons2  26673  diophrw  26715  frgrancvvdeqlem4  28144  pol0N  30403
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-in 3295
  Copyright terms: Public domain W3C validator