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

Theorem eleq1a 2352
Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
eleq1a  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )

Proof of Theorem eleq1a
StepHypRef Expression
1 eleq1 2343 . 2  |-  ( C  =  A  ->  ( C  e.  B  <->  A  e.  B ) )
21biimprcd 216 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  elex22  2799  elex2  2800  reu6  2954  disjne  3500  peano5  4679  ssimaex  5584  fnex  5741  f1ocnv2d  6068  tfrlem8  6400  tz7.48-2  6454  tz7.49  6457  eroprf  6756  onfin  7051  pssnn  7081  ac6sfi  7101  elfiun  7183  brwdom  7281  ficardom  7594  ficard  8187  tskxpss  8394  inar1  8397  rankcf  8399  tskuni  8405  gruun  8428  nsmallnq  8601  prnmadd  8621  genpss  8628  renegcli  9108  supmul1  9719  supmullem2  9721  supmul  9722  nn0ind-raph  10112  uzwo  10281  uzwoOLD  10282  iccid  10701  mertenslem2  12341  4sqlem1  12995  4sqlem4  12999  4sqlem11  13002  odlem1  14850  gexlem1  14890  lssneln0  15709  lss1d  15720  lspsn  15759  lsmelval2  15838  opnneiid  16863  cmpsublem  17126  metrest  18070  dscopn  18096  ovolshftlem2  18869  subopnmbl  18959  deg1ldgn  19479  plyremlem  19684  coseq0negpitopi  19871  ppiublem1  20441  shsleji  21949  spansnss  22150  spansncvi  22231  f1o3d  23037  sigaclcu2  23481  measdivcstOLD  23551  measdivcst  23552  dfon2lem6  24144  bdayfo  24329  altxpsspw  24511  mptelee  24523  hfun  24808  ontgval  24870  ordtoplem  24874  ordcmp  24886  findreccl  24892  grpodivfo  25374  intopcoaconb  25540  qusp  25542  cntrset  25602  heibor1lem  26533  heibor1  26534  hbtlem2  27328  hbtlem5  27332  symggen  27411  psgnghm  27437  fveqvfvv  27987  afv0fv0  28012  snssiALTVD  28602  snssiALT  28603  elex2VD  28614  elex22VD  28615  lshpkrlem1  29300  lfl1dim  29311  leat3  29485  meetat2  29487  glbconxN  29567  pointpsubN  29940  pmapglbx  29958  linepsubclN  30140  dia2dimlem7  31260  dib1dim2  31358  diclspsn  31384  dih1dimatlem  31519  dihatexv2  31529  djhlsmcl  31604
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-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator