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

Theorem ineq1 4166
Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) (Proof shortened by SN, 20-Sep-2023.)
Assertion
Ref Expression
ineq1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem ineq1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 rabeq 3469 . 2 (𝐴 = 𝐵 → {𝑥𝐴𝑥𝐶} = {𝑥𝐵𝑥𝐶})
2 dfin5 3927 . 2 (𝐴𝐶) = {𝑥𝐴𝑥𝐶}
3 dfin5 3927 . 2 (𝐵𝐶) = {𝑥𝐵𝑥𝐶}
41, 2, 33eqtr4g 2884 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  {crab 3137  cin 3918
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-in 3926
This theorem is referenced by:  ineq2  4168  ineq12  4169  ineq1i  4170  ineq1d  4173  unineq  4239  dfrab3ss  4266  disjeq0  4388  intprg  4896  inex1g  5210  reseq1  5836  sspred  6145  isofrlem  7088  qsdisj  8372  fiint  8794  elfiun  8893  dffi3  8894  inf3lema  9086  dfac5lem5  9553  kmlem12  9587  kmlem14  9589  fin23lem24  9744  fin23lem26  9747  fin23lem23  9748  fin23lem22  9749  fin23lem27  9750  ingru  10237  uzin2  14706  incexclem  15193  elrestr  16704  firest  16708  inopn  21513  isbasisg  21561  basis1  21564  basis2  21565  tgval  21569  fctop  21618  cctop  21620  ntrfval  21638  elcls  21687  clsndisj  21689  elcls3  21697  neindisj2  21737  tgrest  21773  restco  21778  restsn  21784  restcld  21786  restcldi  21787  restopnb  21789  neitr  21794  restcls  21795  ordtbaslem  21802  ordtrest2lem  21817  hausnei2  21967  cnhaus  21968  regsep2  21990  dishaus  21996  ordthauslem  21997  cmpsublem  22013  cmpsub  22014  nconnsubb  22037  connsubclo  22038  1stcelcls  22075  islly  22082  cldllycmp  22109  lly1stc  22110  locfincmp  22140  elkgen  22150  ptclsg  22229  dfac14lem  22231  txrest  22245  pthaus  22252  txhaus  22261  xkohaus  22267  xkoptsub  22268  regr1lem  22353  isfbas  22443  fbasssin  22450  fbun  22454  isfil  22461  fbunfip  22483  fgval  22484  filconn  22497  uzrest  22511  isufil2  22522  hauspwpwf1  22601  fclsopni  22629  fclsnei  22633  fclsrest  22638  fcfnei  22649  fcfneii  22651  tsmsfbas  22742  ustincl  22822  ustdiag  22823  ustinvel  22824  ustexhalf  22825  ust0  22834  trust  22844  restutopopn  22853  lpbl  23119  methaus  23136  metrest  23140  restmetu  23186  qtopbaslem  23373  qdensere  23384  xrtgioo  23420  metnrmlem3  23475  icoopnst  23553  iocopnst  23554  ovolicc2lem2  24131  ovolicc2lem5  24134  mblsplit  24145  limcnlp  24490  ellimc3  24491  limcflf  24493  limciun  24506  ig1pval  24782  shincl  29173  shmodi  29182  omlsi  29196  pjoml  29228  chm0  29283  chincl  29291  chdmm1  29317  ledi  29332  cmbr  29376  cmbr3  29400  mdbr  30086  dmdmd  30092  dmdi  30094  dmdbr3  30097  dmdbr4  30098  mdslmd1lem4  30120  cvmd  30128  cvexch  30166  dmdbr6ati  30215  mddmdin0i  30223  difeq  30298  ofpreima2  30430  rspectopn  31200  ordtrest2NEWlem  31250  inelsros  31522  diffiunisros  31523  measvuni  31558  measinb  31565  inelcarsg  31654  carsgclctunlem2  31662  totprob  31770  ballotlemgval  31866  cvmscbv  32590  cvmsdisj  32602  cvmsss2  32606  satfv1  32695  nepss  33033  brapply  33484  opnbnd  33758  isfne  33772  tailfb  33810  bj-restsn  34469  bj-restpw  34479  bj-rest0  34480  bj-restb  34481  nlpfvineqsn  34798  fvineqsnf1  34799  pibt2  34806  ptrest  35028  poimirlem30  35059  mblfinlem2  35067  bndss  35196  qsdisjALTV  35982  redundss3  35995  lcvexchlem4  36305  fipjust  40208  ntrkbimka  40688  ntrk0kbimka  40689  clsk3nimkb  40690  isotone2  40699  ntrclskb  40719  ntrclsk3  40720  ntrclsk13  40721  elrestd  41694  islptre  42214  islpcn  42234  subsaliuncllem  42950  subsaliuncl  42951  nnfoctbdjlem  43047  caragensplit  43092  vonvolmbllem  43252  vonvolmbl  43253  incsmflem  43328  decsmflem  43352  smflimlem2  43358  smflimlem3  43359  smflim  43363  smfpimcclem  43391  uzlidlring  44506  rngcvalALTV  44538  rngcval  44539  ringcvalALTV  44584  ringcval  44585
  Copyright terms: Public domain W3C validator