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

Theorem ineq2i 3367
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 3364 . 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 1623    i^i cin 3151
This theorem is referenced by:  in4  3385  inindir  3387  indif2  3412  difun1  3428  dfrab3ss  3446  undif1  3529  difdifdir  3541  dfif3  3575  dfif5  3577  intunsn  3901  rint0  3902  riin0  3975  resiundiOLD  4745  res0  4959  resres  4968  resundi  4969  resindi  4971  inres  4973  resiun2  4975  resopab  4996  dffr3  5045  dfse2  5046  dminxp  5118  imainrect  5119  resdmres  5164  funimacnv  5324  fresaun  5412  fresaunres2  5413  tfrlem10  6403  sbthlem5  6975  dfsup2  7195  dfsup2OLD  7196  dfsup3OLD  7197  wemapwe  7400  epfrs  7413  en3lplem2  7417  r0weon  7640  infxpenlem  7641  kmlem11  7786  ackbij1lem1  7846  ackbij1lem2  7847  axdc3lem4  8079  canthwelem  8272  dmaddpi  8514  dmmulpi  8515  ssxr  8892  fz1isolem  11399  fsumiun  12279  sadeq  12663  bitsres  12664  smuval2  12673  smumul  12684  ressinbas  13204  sylow2a  14930  lsmmod2  14985  lsmdisj2r  14994  ablfac1eu  15308  ressmplbas2  16199  opsrtoslem1  16225  pjdm  16607  rintopn  16655  ordtrest2  16934  cmpsublem  17126  kgentopon  17233  hausdiag  17339  uzrest  17592  ufprim  17604  metnrmlem3  18365  clsocv  18677  ismbl  18885  unmbl  18895  volinun  18903  voliunlem1  18907  ovolioo  18925  itg2cnlem2  19117  ellimc2  19227  limcflf  19231  lhop1lem  19360  lgsquadlem3  20595  rplogsum  20676  ex-in  20812  chdmj3i  22062  chdmj4i  22063  chjassi  22065  pjoml2i  22164  pjoml3i  22165  cmcmlem  22170  cmcm2i  22172  cmbr3i  22179  fh3i  22202  fh4i  22203  osumcor2i  22223  mayetes3i  22309  mdslmd3i  22912  mdexchi  22915  atabsi  22981  dmdbr5ati  23002  inin  23167  dmhashres  23174  hasheuni  23453  cvmscld  23804  dfpo2  24112  elrn3  24120  dfpred2  24175  predidm  24188  wfrlem13  24268  isunscov  25074  inabs2  25138  empos  25242  inposet  25278  dispos  25287  islimrs4  25582  bwt2  25592  hdrmp  25706  mapfzcons2  26796  diophrw  26838  f1oun2prg  28076  pol0N  30098
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator