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

Theorem eleq1a 2526
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 2519 . 2  |-  ( C  =  A  ->  ( C  e.  B  <->  A  e.  B ) )
21biimprcd 229 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1446    e. wcel 1889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1666  df-cleq 2446  df-clel 2449
This theorem is referenced by:  elex2  3060  elex22  3061  reu6  3229  disjne  3812  ssimaex  5935  fnex  6137  f1ocnv2d  6525  peano5  6721  tfrlem8  7107  tz7.48-2  7164  tz7.49  7167  eroprf  7466  onfin  7768  pssnn  7795  ac6sfi  7820  elfiun  7949  brwdom  8087  ficardom  8400  ficard  8995  tskxpss  9202  inar1  9205  rankcf  9207  tskuni  9213  gruun  9236  nsmallnq  9407  prnmadd  9427  genpss  9434  eqlei  9749  eqlei2  9750  renegcli  9940  supaddc  10581  supadd  10582  supmul1  10583  supmullem2  10585  supmul  10586  nn0ind-raph  11042  uzwo  11229  iccid  11688  hashvnfin  12548  brfi1indlem  12656  mertenslem2  13953  4sqlem1  14904  4sqlem4  14908  4sqlem11  14911  symggen  17123  psgnran  17168  odlem1  17193  odlem1OLD  17196  gexlem1  17240  gexlem1OLD  17242  lssneln0  18187  lss1d  18198  lspsn  18237  lsmelval2  18320  psgnghm  19160  opnneiid  20154  cmpsublem  20426  metrest  21551  metustel  21577  dscopn  21600  ovolshftlem2  22475  subopnmbl  22574  deg1ldgn  23054  plyremlem  23269  coseq0negpitopi  23470  ppiublem1  24142  mptelee  24937  frgrancvvdeqlem1  25770  frgrawopreglem4  25787  shsleji  27035  spansnss  27236  spansncvi  27317  f1o3d  28241  sigaclcu2  28954  measdivcstOLD  29058  dfon2lem6  30446  bdayfo  30576  altxpsspw  30756  hfun  30957  ontgval  31103  ordtoplem  31107  ordcmp  31119  findreccl  31125  bj-xpnzex  31564  bj-snsetex  31569  topdifinfindis  31761  finxpreclem1  31793  ovoliunnfl  31994  volsupnfl  31997  heibor1lem  32153  heibor1  32154  lshpkrlem1  32688  lfl1dim  32699  leat3  32873  meetat2  32875  glbconxN  32955  pointpsubN  33328  pmapglbx  33346  linepsubclN  33528  dia2dimlem7  34650  dib1dim2  34748  diclspsn  34774  dih1dimatlem  34909  dihatexv2  34919  djhlsmcl  34994  hbtlem2  35995  hbtlem5  35999  rp-isfinite6  36175  snssiALTVD  37233  snssiALT  37234  elex2VD  37244  elex22VD  37245  fveqvfvv  38635  afv0fv0  38661  lswn0  38930  clel5  38991  nbuhgr2vtx1edgblem  39429  lidlmmgm  40029  1neven  40036  cznrng  40061  gsumpr  40246
  Copyright terms: Public domain W3C validator