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

Theorem ineq2i 3540
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 3537 . 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 1653    i^i cin 3320
This theorem is referenced by:  in4  3558  inindir  3560  indif2  3585  difun1  3602  dfrab3ss  3620  undif1  3704  difdifdir  3716  dfif3  3750  dfif5  3752  intunsn  4090  rint0  4091  riin0  4165  res0  5151  resres  5160  resundi  5161  resindi  5163  inres  5165  resiun2  5167  resopab  5188  dffr3  5237  dfse2  5238  dminxp  5312  imainrect  5313  resdmres  5362  funimacnv  5526  fresaun  5615  fresaunres2  5616  tfrlem10  6649  sbthlem5  7222  infssuni  7398  dfsup2  7448  dfsup2OLD  7449  dfsup3OLD  7450  wemapwe  7655  epfrs  7668  en3lplem2  7672  r0weon  7895  infxpenlem  7896  kmlem11  8041  ackbij1lem1  8101  ackbij1lem2  8102  axdc3lem4  8334  canthwelem  8526  dmaddpi  8768  dmmulpi  8769  ssxr  9146  fz1isolem  11711  f1oun2prg  11865  fsumiun  12601  sadeq  12985  bitsres  12986  smuval2  12995  smumul  13006  ressinbas  13526  sylow2a  15254  lsmmod2  15309  lsmdisj2r  15318  ablfac1eu  15632  ressmplbas2  16519  opsrtoslem1  16545  pjdm  16935  rintopn  16983  ordtrest2  17269  cmpsublem  17463  bwth  17474  kgentopon  17571  hausdiag  17678  uzrest  17930  ufprim  17942  trust  18260  metnrmlem3  18892  clsocv  19205  ismbl  19423  unmbl  19433  volinun  19441  voliunlem1  19445  ovolioo  19463  itg2cnlem2  19655  ellimc2  19765  limcflf  19769  lhop1lem  19898  lgsquadlem3  21141  rplogsum  21222  0pth  21571  1pthonlem2  21591  ex-in  21734  chdmj3i  22986  chdmj4i  22987  chjassi  22989  pjoml2i  23088  pjoml3i  23089  cmcmlem  23094  cmcm2i  23096  cmbr3i  23103  fh3i  23126  fh4i  23127  osumcor2i  23147  mayetes3i  23233  mdslmd3i  23836  mdexchi  23839  atabsi  23905  dmdbr5ati  23926  inin  23997  dmhashres  24158  hasheuni  24476  cvmscld  24961  dfpo2  25379  elrn3  25387  dfpred2  25449  predidm  25464  wfrlem13  25551  mblfinlem2  26245  ftc1anclem6  26286  mapfzcons2  26776  diophrw  26818  frgrancvvdeqlem4  28423  pol0N  30707
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-in 3328
  Copyright terms: Public domain W3C validator