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

Theorem ineq2i 3773
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 3770 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  cin 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547
This theorem is referenced by:  in4  3791  inindir  3793  indif2  3829  difun1  3846  dfrab3ss  3864  undif1  3995  difdifdir  4008  dfif3  4050  dfif5  4052  disjpr2  4194  disjprsn  4196  intunsn  4451  rint0  4452  riin0  4530  csbres  5320  res0  5321  resres  5329  resundi  5330  resindi  5332  inres  5334  resiun2  5338  resopab  5366  dffr3  5417  dfse2  5418  dminxp  5493  imainrect  5494  resdmres  5543  dfpred2  5606  predidm  5619  funimacnv  5884  fresaun  5988  fresaunres2  5989  wfrlem13  7314  tfrlem10  7370  sbthlem5  7959  infssuni  8140  dfsup2  8233  en3lplem2  8395  wemapwe  8477  epfrs  8490  r0weon  8718  infxpenlem  8719  kmlem11  8865  ackbij1lem1  8925  ackbij1lem2  8926  axdc3lem4  9158  canthwelem  9351  dmaddpi  9591  dmmulpi  9592  ssxr  9986  dmhashres  12991  fz1isolem  13102  f1oun2prg  13512  fsumiun  14394  sadeq  15032  bitsres  15033  smuval2  15042  smumul  15053  ressinbas  15763  lubdm  16802  glbdm  16815  sylow2a  17857  lsmmod2  17912  lsmdisj2r  17921  ablfac1eu  18295  ressmplbas2  19276  opsrtoslem1  19305  pjdm  19870  rintopn  20539  ordtrest2  20818  cmpsublem  21012  kgentopon  21151  hausdiag  21258  uzrest  21511  ufprim  21523  trust  21843  metnrmlem3  22472  clsocv  22857  ismbl  23101  unmbl  23112  volinun  23121  voliunlem1  23125  ovolioo  23143  itg2cnlem2  23335  ellimc2  23447  limcflf  23451  lhop1lem  23580  lgsquadlem3  24907  rplogsum  25016  umgrislfupgrlem  25788  0pth  26100  1pthonlem2  26120  frgrancvvdeqlem4  26560  ex-in  26674  chdmj3i  27726  chdmj4i  27727  chjassi  27729  pjoml2i  27828  pjoml3i  27829  cmcmlem  27834  cmcm2i  27836  cmbr3i  27843  fh3i  27866  fh4i  27867  osumcor2i  27887  mayetes3i  27972  mdslmd3i  28575  mdexchi  28578  atabsi  28644  dmdbr5ati  28665  inin  28737  uniin2  28751  ordtrest2NEW  29297  hasheuni  29474  carsgclctunlem1  29706  eulerpartgbij  29761  fiblem  29787  cvmscld  30509  msrid  30696  dfpo2  30898  elrn3  30906  bj-inrab3  32117  poimirlem15  32594  mblfinlem2  32617  ftc1anclem6  32660  pol0N  34213  mapfzcons2  36300  diophrw  36340  conrel2d  36975  iunrelexp0  37013  hashnzfz  37541  disjinfi  38375  fourierdlem80  39079  sge0resplit  39299  sge0split  39302  caragenuncllem  39402  sPthisPth  40932  0pth-av  41293  1pthdlem2  41303  frgrncvvdeqlem4  41472
  Copyright terms: Public domain W3C validator