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

Theorem ineq1 3679
Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)
Assertion
Ref Expression
ineq1  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )

Proof of Theorem ineq1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq2 2527 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21anbi1d 702 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  /\  x  e.  C
)  <->  ( x  e.  B  /\  x  e.  C ) ) )
3 elin 3673 . . 3  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
4 elin 3673 . . 3  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
52, 3, 43bitr4g 288 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  i^i  C )  <->  x  e.  ( B  i^i  C ) ) )
65eqrdv 2451 1  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398    e. wcel 1823    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468
This theorem is referenced by:  ineq2  3680  ineq12  3681  ineq1i  3682  ineq1d  3685  unineq  3745  dfrab3ss  3773  intprg  4306  inex1g  4580  reseq1  5256  isofrlem  6211  qsdisj  7380  fiint  7789  elfiun  7882  dffi3  7883  inf3lema  8032  dfac5lem5  8499  kmlem12  8532  kmlem14  8534  fin23lem24  8693  fin23lem26  8696  fin23lem23  8697  fin23lem22  8698  fin23lem27  8699  ingru  9182  uzin2  13262  incexclem  13733  elrestr  14921  firest  14925  inopn  19578  isbasisg  19618  basis1  19621  basis2  19622  tgval  19626  fctop  19675  cctop  19677  ntrfval  19695  elcls  19744  clsndisj  19746  elcls3  19754  neindisj2  19794  tgrest  19830  restco  19835  restsn  19841  restcld  19843  restcldi  19844  restopnb  19846  neitr  19851  restcls  19852  ordtbaslem  19859  ordtrest2lem  19874  hausnei2  20024  cnhaus  20025  regsep2  20047  dishaus  20053  ordthauslem  20054  cmpsublem  20069  cmpsub  20070  nconsubb  20093  consubclo  20094  1stcelcls  20131  islly  20138  cldllycmp  20165  lly1stc  20166  locfincmp  20196  elkgen  20206  ptclsg  20285  dfac14lem  20287  txrest  20301  pthaus  20308  txhaus  20317  xkohaus  20323  xkoptsub  20324  regr1lem  20409  isfbas  20499  fbasssin  20506  fbun  20510  isfil  20517  fbunfip  20539  fgval  20540  filcon  20553  uzrest  20567  isufil2  20578  hauspwpwf1  20657  fclsopni  20685  fclsnei  20689  fclsrest  20694  fcfnei  20705  fcfneii  20707  tsmsfbas  20795  ustincl  20879  ustdiag  20880  ustinvel  20881  ustexhalf  20882  ust0  20891  trust  20901  restutopopn  20910  lpbl  21175  methaus  21192  metrest  21196  restmetu  21259  qtopbaslem  21434  qdensere  21446  xrtgioo  21480  metnrmlem3  21534  icoopnst  21608  iocopnst  21609  ovolicc2lem2  22098  ovolicc2lem5  22101  mblsplit  22112  limcnlp  22451  ellimc3  22452  limcflf  22454  limciun  22467  ig1pval  22742  shincl  26500  shmodi  26509  omlsi  26523  pjoml  26555  chm0  26610  chincl  26618  chdmm1  26644  ledi  26659  cmbr  26703  cmbr3  26727  mdbr  27414  dmdmd  27420  dmdi  27422  dmdbr3  27425  dmdbr4  27426  mdslmd1lem4  27448  cvmd  27456  cvexch  27494  dmdbr6ati  27543  mddmdin0i  27551  difeq  27618  ofpreima2  27738  ordtrest2NEWlem  28142  measvuni  28425  measinb  28432  inelcarsg  28522  carsgclctunlem2  28530  totprob  28633  ballotlemgval  28729  cvmscbv  28970  cvmsdisj  28982  cvmsss2  28986  nepss  29339  sspred  29495  brapply  29819  ptrest  30291  mblfinlem2  30295  opnbnd  30386  isfne  30400  tailfb  30438  bndss  30525  islptre  31867  islpcn  31887  uzlidlring  33008  rngcvalALTV  33042  rngcval  33043  ringcvalALTV  33088  ringcval  33089  lcvexchlem4  35178  fipjust  38182
  Copyright terms: Public domain W3C validator