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

Theorem ineq2i 3789
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 3786 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  cin 3554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562
This theorem is referenced by:  in4  3807  inindir  3809  indif2  3846  difun1  3863  dfrab3ss  3881  undif1  4015  difdifdir  4028  dfif3  4072  dfif5  4074  disjpr2  4218  disjprsn  4220  disjtp2  4222  intunsn  4481  rint0  4482  riin0  4560  csbres  5359  res0  5360  resres  5368  resundi  5369  resindi  5371  inres  5373  resiun2  5377  resopab  5405  dffr3  5457  dfse2  5458  dminxp  5533  imainrect  5534  resdmres  5584  dfpred2  5648  predidm  5661  funimacnv  5928  fresaun  6032  fresaunres2  6033  wfrlem13  7372  tfrlem10  7428  sbthlem5  8018  infssuni  8201  dfsup2  8294  en3lplem2  8456  wemapwe  8538  epfrs  8551  r0weon  8779  infxpenlem  8780  kmlem11  8926  ackbij1lem1  8986  ackbij1lem2  8987  axdc3lem4  9219  canthwelem  9416  dmaddpi  9656  dmmulpi  9657  ssxr  10051  dmhashres  13069  fz1isolem  13183  f1oun2prg  13598  fsumiun  14480  sadeq  15118  bitsres  15119  smuval2  15128  smumul  15139  ressinbas  15857  lubdm  16900  glbdm  16913  sylow2a  17955  lsmmod2  18010  lsmdisj2r  18019  ablfac1eu  18393  ressmplbas2  19374  opsrtoslem1  19403  pjdm  19970  rintopn  20639  ordtrest2  20918  cmpsublem  21112  kgentopon  21251  hausdiag  21358  uzrest  21611  ufprim  21623  trust  21943  metnrmlem3  22572  clsocv  22957  ismbl  23201  unmbl  23212  volinun  23221  voliunlem1  23225  ovolioo  23243  itg2cnlem2  23435  ellimc2  23547  limcflf  23551  lhop1lem  23680  lgsquadlem3  25007  rplogsum  25116  umgrislfupgrlem  25912  spthispth  26491  0pth  26852  1pthdlem2  26862  frgrncvvdeqlem4  27030  ex-in  27136  chdmj3i  28191  chdmj4i  28192  chjassi  28194  pjoml2i  28293  pjoml3i  28294  cmcmlem  28299  cmcm2i  28301  cmbr3i  28308  fh3i  28331  fh4i  28332  osumcor2i  28352  mayetes3i  28437  mdslmd3i  29040  mdexchi  29043  atabsi  29109  dmdbr5ati  29130  inin  29200  uniin2  29214  ordtrest2NEW  29751  hasheuni  29928  carsgclctunlem1  30160  eulerpartgbij  30215  fiblem  30241  cvmscld  30963  msrid  31150  dfpo2  31353  elrn3  31361  noextend  31524  bj-inrab3  32572  poimirlem15  33056  mblfinlem2  33079  ftc1anclem6  33122  pol0N  34675  mapfzcons2  36762  diophrw  36802  conrel2d  37437  iunrelexp0  37475  hashnzfz  38001  disjinfi  38854  fourierdlem80  39710  sge0resplit  39930  sge0split  39933  caragenuncllem  40033
  Copyright terms: Public domain W3C validator