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

Theorem ineq1 3363
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 2344 . . . 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 3358 . . 3  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
4 elin 3358 . . 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 2281 1  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684    i^i cin 3151
This theorem is referenced by:  ineq2  3364  ineq12  3365  ineq1i  3366  ineq1d  3369  unineq  3419  dfrab3ss  3446  intprg  3896  inex1g  4157  reseq1  4949  isofrlem  5837  qsdisj  6736  fiint  7133  elfiun  7183  dffi3  7184  inf3lema  7325  dfac5lem5  7754  kmlem12  7787  kmlem14  7789  fin23lem24  7948  fin23lem26  7951  fin23lem23  7952  fin23lem22  7953  fin23lem27  7954  ingru  8437  uzin2  11828  incexclem  12295  elrestr  13333  firest  13337  inopn  16645  isbasisg  16685  basis1  16688  basis2  16689  tgval  16693  fctop  16741  cctop  16743  ntrfval  16761  elcls  16810  clsndisj  16812  elcls3  16820  neindisj2  16860  tgrest  16890  restco  16895  restsn  16901  restcld  16903  restcldi  16904  restopnb  16906  restcls  16911  ordtbaslem  16918  ordtrest2lem  16933  hausnei2  17081  cnhaus  17082  regsep2  17104  dishaus  17110  ordthauslem  17111  cmpsublem  17126  cmpsub  17127  nconsubb  17149  consubclo  17150  1stcelcls  17187  islly  17194  cldllycmp  17221  lly1stc  17222  elkgen  17231  ptclsg  17309  dfac14lem  17311  txrest  17325  pthaus  17332  txhaus  17341  xkohaus  17347  xkoptsub  17348  regr1lem  17430  isfbas  17524  fbasssin  17531  fbun  17535  isfil  17542  fbunfip  17564  fgval  17565  filcon  17578  uzrest  17592  isufil2  17603  hauspwpwf1  17682  fclsopni  17710  fclsnei  17714  fclsrest  17719  fcfnei  17730  fcfneii  17732  tsmsfbas  17810  lpbl  18049  methaus  18066  metrest  18070  qtopbaslem  18267  qdensere  18279  xrtgioo  18312  metnrmlem3  18365  icoopnst  18437  iocopnst  18438  ovolicc2lem2  18877  ovolicc2lem5  18880  mblsplit  18891  limcnlp  19228  ellimc3  19229  limcflf  19231  limciun  19244  ig1pval  19558  shincl  21960  shmodi  21969  omlsi  21983  pjoml  22015  chm0  22070  chincl  22078  chdmm1  22104  ledi  22119  cmbr  22163  cmbr3  22187  mdbr  22874  dmdmd  22880  dmdi  22882  dmdbr3  22885  dmdbr4  22886  mdslmd1lem4  22908  cvmd  22916  cvexch  22954  dmdbr6ati  23003  mddmdin0i  23011  ballotlemgval  23082  difeq  23128  measvuni  23542  measinb  23548  totprob  23630  cvmscbv  23789  cvmsdisj  23801  cvmsss2  23805  nepss  24072  predeq2  24170  sspred  24174  brapply  24477  neiopne  25051  basexre  25522  cnfilca  25556  islimrs3  25581  islimrs4  25582  bwt2  25592  hdrmp  25706  selsubf3g  25992  indcls2  25996  pgapspf2  26053  nbssntrs  26147  opnbnd  26243  isfne  26268  locfincmp  26304  tailfb  26326  bndss  26510  lcvexchlem4  29227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator