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

Theorem ineq1 3535
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 2497 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21anbi1d 686 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  /\  x  e.  C
)  <->  ( x  e.  B  /\  x  e.  C ) ) )
3 elin 3530 . . 3  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
4 elin 3530 . . 3  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
52, 3, 43bitr4g 280 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  i^i  C )  <->  x  e.  ( B  i^i  C ) ) )
65eqrdv 2434 1  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725    i^i cin 3319
This theorem is referenced by:  ineq2  3536  ineq12  3537  ineq1i  3538  ineq1d  3541  unineq  3591  dfrab3ss  3619  intprg  4084  inex1g  4346  reseq1  5140  isofrlem  6060  qsdisj  6981  fiint  7383  elfiun  7435  dffi3  7436  inf3lema  7579  dfac5lem5  8008  kmlem12  8041  kmlem14  8043  fin23lem24  8202  fin23lem26  8205  fin23lem23  8206  fin23lem22  8207  fin23lem27  8208  ingru  8690  uzin2  12148  incexclem  12616  elrestr  13656  firest  13660  inopn  16972  isbasisg  17012  basis1  17015  basis2  17016  tgval  17020  fctop  17068  cctop  17070  ntrfval  17088  elcls  17137  clsndisj  17139  elcls3  17147  neindisj2  17187  tgrest  17223  restco  17228  restsn  17234  restcld  17236  restcldi  17237  restopnb  17239  neitr  17244  restcls  17245  ordtbaslem  17252  ordtrest2lem  17267  hausnei2  17417  cnhaus  17418  regsep2  17440  dishaus  17446  ordthauslem  17447  cmpsublem  17462  cmpsub  17463  bwth  17473  nconsubb  17486  consubclo  17487  1stcelcls  17524  islly  17531  cldllycmp  17558  lly1stc  17559  elkgen  17568  ptclsg  17647  dfac14lem  17649  txrest  17663  pthaus  17670  txhaus  17679  xkohaus  17685  xkoptsub  17686  regr1lem  17771  isfbas  17861  fbasssin  17868  fbun  17872  isfil  17879  fbunfip  17901  fgval  17902  filcon  17915  uzrest  17929  isufil2  17940  hauspwpwf1  18019  fclsopni  18047  fclsnei  18051  fclsrest  18056  fcfnei  18067  fcfneii  18069  tsmsfbas  18157  ustincl  18237  ustdiag  18238  ustinvel  18239  ustexhalf  18240  ust0  18249  trust  18259  restutopopn  18268  lpbl  18533  methaus  18550  metrest  18554  restmetu  18617  qtopbaslem  18792  qdensere  18804  xrtgioo  18837  metnrmlem3  18891  icoopnst  18964  iocopnst  18965  ovolicc2lem2  19414  ovolicc2lem5  19417  mblsplit  19428  limcnlp  19765  ellimc3  19766  limcflf  19768  limciun  19781  ig1pval  20095  shincl  22883  shmodi  22892  omlsi  22906  pjoml  22938  chm0  22993  chincl  23001  chdmm1  23027  ledi  23042  cmbr  23086  cmbr3  23110  mdbr  23797  dmdmd  23803  dmdi  23805  dmdbr3  23808  dmdbr4  23809  mdslmd1lem4  23831  cvmd  23839  cvexch  23877  dmdbr6ati  23926  mddmdin0i  23934  difeq  23998  measvuni  24568  measinb  24575  sibfof  24654  totprob  24685  ballotlemgval  24781  cvmscbv  24945  cvmsdisj  24957  cvmsss2  24961  nepss  25175  sspred  25447  brapply  25783  mblfinlem2  26244  opnbnd  26328  isfne  26348  locfincmp  26384  tailfb  26406  bndss  26495  lcvexchlem4  29835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327
  Copyright terms: Public domain W3C validator