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 835  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  5537  res0  5538  resres  5550  resundi  5551  resindi  5553  inres  5555  resiun2  5559  resopab  5587  dffr3  5639  dfse2  5640  dminxp  5715  imainrect  5716  resdmres  5769  dfpred2  5832  predidm  5845  funimacnv  6110  fresaun  6215  fresaunres2  6216  wfrlem13  7580  tfrlem10  7636  sbthlem5  8230  infssuni  8413  dfsup2  8506  en3lplem2  8672  wemapwe  8758  epfrs  8771  r0weon  9035  infxpenlem  9036  kmlem11  9184  ackbij1lem1  9244  ackbij1lem2  9245  axdc3lem4  9477  canthwelem  9674  dmaddpi  9914  dmmulpi  9915  ssxr  10309  dmhashres  13333  fz1isolem  13447  f1oun2prg  13871  fsumiun  14760  sadeq  15402  bitsres  15403  smuval2  15412  smumul  15423  ressinbas  16143  lubdm  17187  glbdm  17200  sylow2a  18241  lsmmod2  18296  lsmdisj2r  18305  ablfac1eu  18680  ressmplbas2  19670  opsrtoslem1  19699  pjdm  20268  rintopn  20934  ordtrest2  21229  cmpsublem  21423  kgentopon  21562  hausdiag  21669  uzrest  21921  ufprim  21933  trust  22253  metnrmlem3  22884  clsocv  23268  ismbl  23514  unmbl  23525  volinun  23534  voliunlem1  23538  ovolioo  23556  itg2cnlem2  23749  ellimc2  23861  limcflf  23865  lhop1lem  23996  lgsquadlem3  25328  rplogsum  25437  umgrislfupgrlem  26238  spthispth  26857  0pth  27305  1pthdlem2  27316  frgrncvvdeqlem3  27483  ex-in  27624  chdmj3i  28682  chdmj4i  28683  chjassi  28685  pjoml2i  28784  pjoml3i  28785  cmcmlem  28790  cmcm2i  28792  cmbr3i  28799  fh3i  28822  fh4i  28823  osumcor2i  28843  mayetes3i  28928  mdslmd3i  29531  mdexchi  29534  atabsi  29600  dmdbr5ati  29621  inin  29690  uniin2  29706  ordtrest2NEW  30309  hasheuni  30487  carsgclctunlem1  30719  eulerpartgbij  30774  fiblem  30800  cvmscld  31593  msrid  31780  dfpo2  31983  elrn3  31990  noextend  32156  noextendseq  32157  madeval2  32273  bj-inrab3  33257  poimirlem15  33757  mblfinlem2  33780  ftc1anclem6  33822  xrnres2  34503  pol0N  35717  mapfzcons2  37808  diophrw  37848  conrel2d  38482  iunrelexp0  38520  hashnzfz  39045  disjinfi  39900  fourierdlem80  40920  sge0resplit  41140  sge0split  41143  caragenuncllem  41246
  Copyright terms: Public domain W3C validator