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

Theorem ineq1 4140
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 3419 . 2 (𝐴 = 𝐵 → {𝑥𝐴𝑥𝐶} = {𝑥𝐵𝑥𝐶})
2 dfin5 3896 . 2 (𝐴𝐶) = {𝑥𝐴𝑥𝐶}
3 dfin5 3896 . 2 (𝐵𝐶) = {𝑥𝐵𝑥𝐶}
41, 2, 33eqtr4g 2804 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2107  {crab 3069  cin 3887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3895
This theorem is referenced by:  ineq2  4141  ineq12  4142  ineq1i  4143  ineq1d  4146  unineq  4212  dfrab3ss  4247  disjeq0  4390  intprgOLD  4916  inex1g  5244  reseq1  5888  sspred  6215  isofrlem  7220  qsdisj  8592  fiint  9100  elfiun  9198  dffi3  9199  inf3lema  9391  dfac5lem5  9892  kmlem12  9926  kmlem14  9928  fin23lem24  10087  fin23lem26  10090  fin23lem23  10091  fin23lem22  10092  fin23lem27  10093  ingru  10580  uzin2  15065  incexclem  15557  elrestr  17148  firest  17152  inopn  22057  isbasisg  22106  basis1  22109  basis2  22110  tgval  22114  fctop  22163  cctop  22165  ntrfval  22184  elcls  22233  clsndisj  22235  elcls3  22243  neindisj2  22283  tgrest  22319  restco  22324  restsn  22330  restcld  22332  restcldi  22333  restopnb  22335  neitr  22340  restcls  22341  ordtbaslem  22348  ordtrest2lem  22363  hausnei2  22513  cnhaus  22514  regsep2  22536  dishaus  22542  ordthauslem  22543  cmpsublem  22559  cmpsub  22560  nconnsubb  22583  connsubclo  22584  1stcelcls  22621  islly  22628  cldllycmp  22655  lly1stc  22656  locfincmp  22686  elkgen  22696  ptclsg  22775  dfac14lem  22777  txrest  22791  pthaus  22798  txhaus  22807  xkohaus  22813  xkoptsub  22814  regr1lem  22899  isfbas  22989  fbasssin  22996  fbun  23000  isfil  23007  fbunfip  23029  fgval  23030  filconn  23043  uzrest  23057  isufil2  23068  hauspwpwf1  23147  fclsopni  23175  fclsnei  23179  fclsrest  23184  fcfnei  23195  fcfneii  23197  tsmsfbas  23288  ustincl  23368  ustdiag  23369  ustinvel  23370  ustexhalf  23371  ust0  23380  trust  23390  restutopopn  23399  lpbl  23668  methaus  23685  metrest  23689  restmetu  23735  qtopbaslem  23931  qdensere  23942  xrtgioo  23978  metnrmlem3  24033  icoopnst  24111  iocopnst  24112  ovolicc2lem2  24691  ovolicc2lem5  24694  mblsplit  24705  limcnlp  25051  ellimc3  25052  limcflf  25054  limciun  25067  ig1pval  25346  shincl  29752  shmodi  29761  omlsi  29775  pjoml  29807  chm0  29862  chincl  29870  chdmm1  29896  ledi  29911  cmbr  29955  cmbr3  29979  mdbr  30665  dmdmd  30671  dmdi  30673  dmdbr3  30676  dmdbr4  30677  mdslmd1lem4  30699  cvmd  30707  cvexch  30745  dmdbr6ati  30794  mddmdin0i  30802  difeq  30874  ofpreima2  31012  rspectopn  31826  ordtrest2NEWlem  31881  inelsros  32155  diffiunisros  32156  measvuni  32191  measinb  32198  inelcarsg  32287  carsgclctunlem2  32295  totprob  32403  ballotlemgval  32499  cvmscbv  33229  cvmsdisj  33241  cvmsss2  33245  satfv1  33334  nepss  33671  brapply  34249  opnbnd  34523  isfne  34537  tailfb  34575  bj-restsn  35262  bj-restpw  35272  bj-rest0  35273  bj-restb  35274  nlpfvineqsn  35589  fvineqsnf1  35590  pibt2  35597  ptrest  35785  poimirlem30  35816  mblfinlem2  35824  bndss  35953  qsdisjALTV  36735  redundss3  36748  lcvexchlem4  37058  fipjust  41179  ntrkbimka  41655  ntrk0kbimka  41656  clsk3nimkb  41657  isotone2  41666  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  ismnushort  41926  elrestd  42665  islptre  43167  islpcn  43187  subsaliuncllem  43903  subsaliuncl  43904  nnfoctbdjlem  44000  caragensplit  44045  vonvolmbllem  44205  vonvolmbl  44206  incsmflem  44286  decsmflem  44311  smflimlem2  44317  smflimlem3  44318  smflim  44322  smfpimcclem  44351  uzlidlring  45498  rngcvalALTV  45530  rngcval  45531  ringcvalALTV  45576  ringcval  45577  sepfsepc  46232  iscnrm3rlem2  46246  iscnrm3rlem8  46252  iscnrm3llem2  46255
  Copyright terms: Public domain W3C validator