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

Theorem ineq2i 3667
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 3664 . 2  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
31, 2ax-mp 5 1  |-  ( C  i^i  A )  =  ( C  i^i  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    i^i cin 3441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449
This theorem is referenced by:  in4  3684  inindir  3686  indif2  3722  difun1  3739  dfrab3ss  3757  undif1  3876  difdifdir  3889  dfif3  3929  dfif5  3931  intunsn  4298  rint0  4299  riin0  4376  csbres  5128  res0  5129  resres  5137  resundi  5138  resindi  5140  inres  5142  resiun2  5144  resopab  5171  dffr3  5221  dfse2  5222  dminxp  5297  imainrect  5298  resdmres  5346  dfpred2  5408  predidm  5421  funimacnv  5673  fresaun  5771  fresaunres2  5772  wfrlem13  7056  tfrlem10  7113  sbthlem5  7692  infssuni  7871  dfsup2  7964  en3lplem2  8120  wemapwe  8201  epfrs  8214  r0weon  8442  infxpenlem  8443  kmlem11  8588  ackbij1lem1  8648  ackbij1lem2  8649  axdc3lem4  8881  canthwelem  9074  dmaddpi  9314  dmmulpi  9315  ssxr  9702  dmhashres  12521  fz1isolem  12619  f1oun2prg  12981  fsumiun  13859  sadeq  14420  bitsres  14421  smuval2  14430  smumul  14441  ressinbas  15147  lubdm  16176  glbdm  16189  sylow2a  17206  lsmmod2  17261  lsmdisj2r  17270  ablfac1eu  17641  ressmplbas2  18614  opsrtoslem1  18642  pjdm  19201  rintopn  19870  ordtrest2  20151  cmpsublem  20345  kgentopon  20484  hausdiag  20591  uzrest  20843  ufprim  20855  trust  21175  metnrmlem3  21789  clsocv  22114  ismbl  22357  unmbl  22368  volinun  22376  voliunlem1  22380  ovolioo  22398  itg2cnlem2  22597  ellimc2  22709  limcflf  22713  lhop1lem  22842  lgsquadlem3  24147  rplogsum  24228  0pth  25145  1pthonlem2  25165  frgrancvvdeqlem4  25606  ex-in  25720  chdmj3i  26971  chdmj4i  26972  chjassi  26974  pjoml2i  27073  pjoml3i  27074  cmcmlem  27079  cmcm2i  27081  cmbr3i  27088  fh3i  27111  fh4i  27112  osumcor2i  27132  mayetes3i  27217  mdslmd3i  27820  mdexchi  27823  atabsi  27889  dmdbr5ati  27910  inin  27985  uniin2  28004  ordtrest2NEW  28568  hasheuni  28745  carsgclctunlem1  28978  eulerpartgbij  29031  fiblem  29057  cvmscld  29784  msrid  29971  dfpo2  30182  elrn3  30190  bj-inrab3  31282  poimirlem15  31658  mblfinlem2  31681  ftc1anclem6  31725  pol0N  33182  mapfzcons2  35269  diophrw  35309  conrel2d  35894  iunrelexp0  35932  hashnzfz  36305  disjinfi  37090  fourierdlem80  37617  sge0resplit  37781  sge0split  37784  caragenuncllem  37841
  Copyright terms: Public domain W3C validator