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

Theorem ineq2i 4136
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 4133 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  cin 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888
This theorem is referenced by:  in4  4152  inindir  4154  indif2  4197  difun1  4214  dfrab3ss  4233  undif1  4382  difdifdir  4395  dfif3  4439  dfif5  4441  disjpr2  4609  disjprsn  4610  disjtp2  4612  intunsn  4877  rint0  4878  riin0  4967  csbres  5821  res0  5822  resres  5831  resundi  5832  resindi  5834  inres  5836  resiun2  5839  resopab  5869  dffr3  5929  dfse2  5930  dminxp  6004  imainrect  6005  cnvrescnv  6019  resdmres  6056  dfpred2  6125  predidm  6138  funimacnv  6405  fresaun  6523  fresaunres2  6524  wfrlem13  7950  tfrlem10  8006  sbthlem5  8615  infssuni  8799  dfsup2  8892  en3lplem2  9060  wemapwe  9144  epfrs  9157  r0weon  9423  infxpenlem  9424  kmlem11  9571  ackbij1lem1  9631  ackbij1lem2  9632  axdc3lem4  9864  canthwelem  10061  dmaddpi  10301  dmmulpi  10302  ssxr  10699  dmhashres  13697  fz1isolem  13815  f1oun2prg  14270  fsumiun  15168  sadeq  15811  bitsres  15812  smuval2  15821  smumul  15832  ressinbas  16552  lubdm  17581  glbdm  17594  sylow2a  18736  lsmmod2  18794  lsmdisj2r  18803  ablfac1eu  19188  pjdm  20396  ressmplbas2  20695  opsrtoslem1  20723  rintopn  21514  ordtrest2  21809  cmpsublem  22004  kgentopon  22143  hausdiag  22250  uzrest  22502  ufprim  22514  trust  22835  metnrmlem3  23466  clsocv  23854  ismbl  24130  unmbl  24141  volinun  24150  voliunlem1  24154  ovolioo  24172  itg2cnlem2  24366  ellimc2  24480  limcflf  24484  lhop1lem  24616  lgsquadlem3  25966  rplogsum  26111  umgrislfupgrlem  26915  spthispth  27515  0pth  27910  1pthdlem2  27921  frgrncvvdeqlem3  28086  ex-in  28210  chdmj3i  29266  chdmj4i  29267  chjassi  29269  pjoml2i  29368  pjoml3i  29369  cmcmlem  29374  cmcm2i  29376  cmbr3i  29383  fh3i  29406  fh4i  29407  osumcor2i  29427  mayetes3i  29512  mdslmd3i  30115  mdexchi  30118  atabsi  30184  dmdbr5ati  30205  inin  30286  uniin2  30316  ordtrest2NEW  31276  hasheuni  31454  carsgclctunlem1  31685  eulerpartgbij  31740  fiblem  31766  cvmscld  32633  sate0  32775  msrid  32905  dfpo2  33104  elrn3  33111  noextend  33286  noextendseq  33287  madeval2  33403  bj-inrab3  34371  poimirlem15  35072  mblfinlem2  35095  ftc1anclem6  35135  xrnres2  35811  redundss3  36023  refrelsredund4  36027  pol0N  37205  mapfzcons2  39658  diophrw  39698  conrel2d  40363  iunrelexp0  40401  hashnzfz  41022  disjinfi  41818  fourierdlem80  42826  sge0resplit  43043  sge0split  43046  caragenuncllem  43149
  Copyright terms: Public domain W3C validator