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

Theorem ineq1 3376
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 2357 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21anbi1d 685 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  /\  x  e.  C
)  <->  ( x  e.  B  /\  x  e.  C ) ) )
3 elin 3371 . . 3  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
4 elin 3371 . . 3  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
52, 3, 43bitr4g 279 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  i^i  C )  <->  x  e.  ( B  i^i  C ) ) )
65eqrdv 2294 1  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696    i^i cin 3164
This theorem is referenced by:  ineq2  3377  ineq12  3378  ineq1i  3379  ineq1d  3382  unineq  3432  dfrab3ss  3459  intprg  3912  inex1g  4173  reseq1  4965  isofrlem  5853  qsdisj  6752  fiint  7149  elfiun  7199  dffi3  7200  inf3lema  7341  dfac5lem5  7770  kmlem12  7803  kmlem14  7805  fin23lem24  7964  fin23lem26  7967  fin23lem23  7968  fin23lem22  7969  fin23lem27  7970  ingru  8453  uzin2  11844  incexclem  12311  elrestr  13349  firest  13353  inopn  16661  isbasisg  16701  basis1  16704  basis2  16705  tgval  16709  fctop  16757  cctop  16759  ntrfval  16777  elcls  16826  clsndisj  16828  elcls3  16836  neindisj2  16876  tgrest  16906  restco  16911  restsn  16917  restcld  16919  restcldi  16920  restopnb  16922  restcls  16927  ordtbaslem  16934  ordtrest2lem  16949  hausnei2  17097  cnhaus  17098  regsep2  17120  dishaus  17126  ordthauslem  17127  cmpsublem  17142  cmpsub  17143  nconsubb  17165  consubclo  17166  1stcelcls  17203  islly  17210  cldllycmp  17237  lly1stc  17238  elkgen  17247  ptclsg  17325  dfac14lem  17327  txrest  17341  pthaus  17348  txhaus  17357  xkohaus  17363  xkoptsub  17364  regr1lem  17446  isfbas  17540  fbasssin  17547  fbun  17551  isfil  17558  fbunfip  17580  fgval  17581  filcon  17594  uzrest  17608  isufil2  17619  hauspwpwf1  17698  fclsopni  17726  fclsnei  17730  fclsrest  17735  fcfnei  17746  fcfneii  17748  tsmsfbas  17826  lpbl  18065  methaus  18082  metrest  18086  qtopbaslem  18283  qdensere  18295  xrtgioo  18328  metnrmlem3  18381  icoopnst  18453  iocopnst  18454  ovolicc2lem2  18893  ovolicc2lem5  18896  mblsplit  18907  limcnlp  19244  ellimc3  19245  limcflf  19247  limciun  19260  ig1pval  19574  shincl  21976  shmodi  21985  omlsi  21999  pjoml  22031  chm0  22086  chincl  22094  chdmm1  22120  ledi  22135  cmbr  22179  cmbr3  22203  mdbr  22890  dmdmd  22896  dmdi  22898  dmdbr3  22901  dmdbr4  22902  mdslmd1lem4  22924  cvmd  22932  cvexch  22970  dmdbr6ati  23019  mddmdin0i  23027  ballotlemgval  23098  difeq  23144  measvuni  23557  measinb  23563  totprob  23645  cvmscbv  23804  cvmsdisj  23816  cvmsss2  23820  nepss  24087  predeq2  24241  sspred  24245  brapply  24548  neiopne  25154  basexre  25625  cnfilca  25659  islimrs3  25684  islimrs4  25685  bwt2  25695  hdrmp  25809  selsubf3g  26095  indcls2  26099  pgapspf2  26156  nbssntrs  26250  opnbnd  26346  isfne  26371  locfincmp  26407  tailfb  26429  bndss  26613  lcvexchlem4  29849
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator