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

Theorem ineq2i 3962
Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
Hypothesis
Ref Expression
ineq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
ineq2i (𝐶𝐴) = (𝐶𝐵)

Proof of Theorem ineq2i
StepHypRef Expression
1 ineq1i.1 . 2 𝐴 = 𝐵
2 ineq2 3959 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  cin 3722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730
This theorem is referenced by:  in4  3978  inindir  3980  indif2  4019  difun1  4036  dfrab3ss  4053  undif1  4185  difdifdir  4198  dfif3  4239  dfif5  4241  disjpr2  4385  disjprsn  4386  disjtp2  4388  intunsn  4650  rint0  4651  riin0  4728  csbres  5535  res0  5536  resres  5548  resundi  5549  resindi  5551  inres  5553  resiun2  5557  resopab  5585  dffr3  5637  dfse2  5638  dminxp  5713  imainrect  5714  resdmres  5767  dfpred2  5830  predidm  5843  funimacnv  6108  fresaun  6213  fresaunres2  6214  wfrlem13  7578  tfrlem10  7634  sbthlem5  8228  infssuni  8411  dfsup2  8504  en3lplem2  8670  wemapwe  8756  epfrs  8769  r0weon  9033  infxpenlem  9034  kmlem11  9182  ackbij1lem1  9242  ackbij1lem2  9243  axdc3lem4  9475  canthwelem  9672  dmaddpi  9912  dmmulpi  9913  ssxr  10307  dmhashres  13326  fz1isolem  13440  f1oun2prg  13864  fsumiun  14753  sadeq  15395  bitsres  15396  smuval2  15405  smumul  15416  ressinbas  16136  lubdm  17180  glbdm  17193  sylow2a  18234  lsmmod2  18289  lsmdisj2r  18298  ablfac1eu  18673  ressmplbas2  19663  opsrtoslem1  19692  pjdm  20261  rintopn  20927  ordtrest2  21222  cmpsublem  21416  kgentopon  21555  hausdiag  21662  uzrest  21914  ufprim  21926  trust  22246  metnrmlem3  22877  clsocv  23261  ismbl  23507  unmbl  23518  volinun  23527  voliunlem1  23531  ovolioo  23549  itg2cnlem2  23742  ellimc2  23854  limcflf  23858  lhop1lem  23989  lgsquadlem3  25321  rplogsum  25430  umgrislfupgrlem  26231  spthispth  26850  0pth  27298  1pthdlem2  27309  frgrncvvdeqlem3  27476  ex-in  27617  chdmj3i  28675  chdmj4i  28676  chjassi  28678  pjoml2i  28777  pjoml3i  28778  cmcmlem  28783  cmcm2i  28785  cmbr3i  28792  fh3i  28815  fh4i  28816  osumcor2i  28836  mayetes3i  28921  mdslmd3i  29524  mdexchi  29527  atabsi  29593  dmdbr5ati  29614  inin  29683  uniin2  29699  ordtrest2NEW  30302  hasheuni  30480  carsgclctunlem1  30712  eulerpartgbij  30767  fiblem  30793  cvmscld  31586  msrid  31773  dfpo2  31976  elrn3  31983  noextend  32149  noextendseq  32150  madeval2  32266  bj-inrab3  33250  poimirlem15  33750  mblfinlem2  33773  ftc1anclem6  33815  xrnres2  34496  pol0N  35710  mapfzcons2  37801  diophrw  37841  conrel2d  38475  iunrelexp0  38513  hashnzfz  39038  disjinfi  39893  fourierdlem80  40913  sge0resplit  41133  sge0split  41136  caragenuncllem  41239
  Copyright terms: Public domain W3C validator