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

Theorem eleq1a 2537
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 2526 . 2  |-  ( C  =  A  ->  ( C  e.  B  <->  A  e.  B ) )
21biimprcd 225 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2446  df-clel 2449
This theorem is referenced by:  elex2  3088  elex22  3089  reu6  3253  disjne  3831  ssimaex  5864  fnex  6052  f1ocnv2d  6420  peano5  6608  tfrlem8  6952  tz7.48-2  7006  tz7.49  7009  eroprf  7307  onfin  7611  pssnn  7641  ac6sfi  7666  elfiun  7790  brwdom  7892  ficardom  8241  ficard  8839  tskxpss  9049  inar1  9052  rankcf  9054  tskuni  9060  gruun  9083  nsmallnq  9256  prnmadd  9276  genpss  9283  eqlei  9594  eqlei2  9595  renegcli  9780  supmul1  10405  supmullem2  10407  supmul  10408  nn0ind-raph  10852  uzwo  11027  uzwoOLD  11028  iccid  11455  hashvnfin  12245  brfi1indlem  12335  mertenslem2  13462  4sqlem1  14126  4sqlem4  14130  4sqlem11  14133  symggen  16094  psgnran  16139  odlem1  16158  gexlem1  16198  lssneln0  17155  lss1d  17166  lspsn  17205  lsmelval2  17288  psgnghm  18134  opnneiid  18861  cmpsublem  19133  metrest  20230  metustelOLD  20257  metustel  20258  dscopn  20297  ovolshftlem2  21124  subopnmbl  21216  deg1ldgn  21696  plyremlem  21902  coseq0negpitopi  22097  ppiublem1  22673  mptelee  23292  shsleji  24924  spansnss  25125  spansncvi  25206  f1o3d  26098  sigaclcu2  26707  measdivcstOLD  26782  dfon2lem6  27744  bdayfo  27959  altxpsspw  28151  hfun  28359  ontgval  28420  ordtoplem  28424  ordcmp  28436  findreccl  28442  supaddc  28564  supadd  28565  ovoliunnfl  28580  volsupnfl  28583  heibor1lem  28855  heibor1  28856  hbtlem2  29627  hbtlem5  29631  fveqvfvv  30177  afv0fv0  30202  lswn0  30405  frgrancvvdeqlem1  30770  frgrawopreglem4  30787  gsumpr  30905  snssiALTVD  31880  snssiALT  31881  elex2VD  31891  elex22VD  31892  bj-xpnzex  32768  bj-snsetex  32773  lshpkrlem1  33078  lfl1dim  33089  leat3  33263  meetat2  33265  glbconxN  33345  pointpsubN  33718  pmapglbx  33736  linepsubclN  33918  dia2dimlem7  35038  dib1dim2  35136  diclspsn  35162  dih1dimatlem  35297  dihatexv2  35307  djhlsmcl  35382
  Copyright terms: Public domain W3C validator