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

Theorem ineq1 4170
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 3424 . 2 (𝐴 = 𝐵 → {𝑥𝐴𝑥𝐶} = {𝑥𝐵𝑥𝐶})
2 dfin5 3923 . 2 (𝐴𝐶) = {𝑥𝐴𝑥𝐶}
3 dfin5 3923 . 2 (𝐵𝐶) = {𝑥𝐵𝑥𝐶}
41, 2, 33eqtr4g 2802 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  {crab 3410  cin 3914
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-in 3922
This theorem is referenced by:  ineq2  4171  ineq12  4172  ineq1i  4173  ineq1d  4176  unineq  4242  dfrab3ss  4277  disjeq0  4420  intprgOLD  4950  inex1g  5281  reseq1  5936  sspred  6267  isofrlem  7290  qsdisj  8740  fiint  9275  elfiun  9373  dffi3  9374  inf3lema  9567  dfac5lem5  10070  kmlem12  10104  kmlem14  10106  fin23lem24  10265  fin23lem26  10268  fin23lem23  10269  fin23lem22  10270  fin23lem27  10271  ingru  10758  uzin2  15236  incexclem  15728  elrestr  17317  firest  17321  inopn  22264  isbasisg  22313  basis1  22316  basis2  22317  tgval  22321  fctop  22370  cctop  22372  ntrfval  22391  elcls  22440  clsndisj  22442  elcls3  22450  neindisj2  22490  tgrest  22526  restco  22531  restsn  22537  restcld  22539  restcldi  22540  restopnb  22542  neitr  22547  restcls  22548  ordtbaslem  22555  ordtrest2lem  22570  hausnei2  22720  cnhaus  22721  regsep2  22743  dishaus  22749  ordthauslem  22750  cmpsublem  22766  cmpsub  22767  nconnsubb  22790  connsubclo  22791  1stcelcls  22828  islly  22835  cldllycmp  22862  lly1stc  22863  locfincmp  22893  elkgen  22903  ptclsg  22982  dfac14lem  22984  txrest  22998  pthaus  23005  txhaus  23014  xkohaus  23020  xkoptsub  23021  regr1lem  23106  isfbas  23196  fbasssin  23203  fbun  23207  isfil  23214  fbunfip  23236  fgval  23237  filconn  23250  uzrest  23264  isufil2  23275  hauspwpwf1  23354  fclsopni  23382  fclsnei  23386  fclsrest  23391  fcfnei  23402  fcfneii  23404  tsmsfbas  23495  ustincl  23575  ustdiag  23576  ustinvel  23577  ustexhalf  23578  ust0  23587  trust  23597  restutopopn  23606  lpbl  23875  methaus  23892  metrest  23896  restmetu  23942  qtopbaslem  24138  qdensere  24149  xrtgioo  24185  metnrmlem3  24240  icoopnst  24318  iocopnst  24319  ovolicc2lem2  24898  ovolicc2lem5  24901  mblsplit  24912  limcnlp  25258  ellimc3  25259  limcflf  25261  limciun  25274  ig1pval  25553  shincl  30365  shmodi  30374  omlsi  30388  pjoml  30420  chm0  30475  chincl  30483  chdmm1  30509  ledi  30524  cmbr  30568  cmbr3  30592  mdbr  31278  dmdmd  31284  dmdi  31286  dmdbr3  31289  dmdbr4  31290  mdslmd1lem4  31312  cvmd  31320  cvexch  31358  dmdbr6ati  31407  mddmdin0i  31415  difeq  31487  ofpreima2  31624  rspectopn  32488  ordtrest2NEWlem  32543  inelsros  32817  diffiunisros  32818  measvuni  32853  measinb  32860  inelcarsg  32951  carsgclctunlem2  32959  totprob  33067  ballotlemgval  33163  cvmscbv  33892  cvmsdisj  33904  cvmsss2  33908  satfv1  33997  nepss  34329  brapply  34552  opnbnd  34826  isfne  34840  tailfb  34878  bj-restsn  35582  bj-restpw  35592  bj-rest0  35593  bj-restb  35594  nlpfvineqsn  35909  fvineqsnf1  35910  pibt2  35917  ptrest  36106  poimirlem30  36137  mblfinlem2  36145  bndss  36274  qsdisjALTV  37106  redundss3  37119  lcvexchlem4  37528  fipjust  41911  ntrkbimka  42384  ntrk0kbimka  42385  clsk3nimkb  42386  isotone2  42395  ntrclskb  42415  ntrclsk3  42416  ntrclsk13  42417  ismnushort  42655  elrestd  43392  restsubel  43442  islptre  43934  islpcn  43954  subsaliuncllem  44672  subsaliuncl  44673  nnfoctbdjlem  44770  caragensplit  44815  vonvolmbllem  44975  vonvolmbl  44976  incsmflem  45056  decsmflem  45081  smflimlem2  45087  smflimlem3  45088  smflim  45092  smfpimcclem  45122  uzlidlring  46301  rngcvalALTV  46333  rngcval  46334  ringcvalALTV  46379  ringcval  46380  sepfsepc  47034  iscnrm3rlem2  47048  iscnrm3rlem8  47054  iscnrm3llem2  47057
  Copyright terms: Public domain W3C validator