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

Theorem eleq1a 2839
Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
eleq1a (𝐴𝐵 → (𝐶 = 𝐴𝐶𝐵))

Proof of Theorem eleq1a
StepHypRef Expression
1 eleq1 2832 . 2 (𝐶 = 𝐴 → (𝐶𝐵𝐴𝐵))
21biimprcd 241 1 (𝐴𝐵 → (𝐶 = 𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-clel 2761
This theorem is referenced by:  elex2  3369  elex22  3370  clel5  3497  reu6  3554  disjne  4183  eqoreldif  4382  ordelinel  6006  ssimaex  6452  fnex  6674  f1ocnv2d  7084  peano5  7287  tfrlem8  7684  tz7.48-2  7741  tz7.49  7744  eroprf  8049  onfin  8358  pssnn  8385  ac6sfi  8411  elfiun  8543  brwdom  8679  ficardom  9038  ficard  9640  tskxpss  9847  inar1  9850  rankcf  9852  tskuni  9858  gruun  9881  nsmallnq  10052  prnmadd  10072  genpss  10079  eqlei  10401  eqlei2  10402  renegcli  10596  supaddc  11244  supadd  11245  supmul1  11246  supmullem2  11248  supmul  11249  nn0ind-raph  11724  uzwo  11952  iccid  12422  hashvnfin  13353  hashdifsnp1  13479  mertenslem2  14900  4sqlem1  15931  4sqlem4  15935  4sqlem11  15938  symggen  18153  psgnran  18199  odlem1  18218  gexlem1  18258  lssvneln0  19221  lssneln0OLD  19223  lss1d  19235  lspsn  19274  lsmelval2  19357  psgnghm  20198  opnneiid  21210  cmpsublem  21482  metrest  22608  metustel  22634  dscopn  22657  ovolshftlem2  23568  subopnmbl  23662  deg1ldgn  24144  plyremlem  24350  coseq0negpitopi  24547  ppiublem1  25218  mptelee  26066  nbuhgr2vtx1edgblem  26526  clwwlknonwwlknonbOLD  27380  numclwwlk1lem2foa  27645  numclwwlk1lem2foaOLD  27646  shsleji  28685  spansnss  28886  spansncvi  28967  f1o3d  29881  sigaclcu2  30630  measdivcstOLD  30734  dfon2lem6  32136  noextendseq  32264  bdayfo  32272  scutf  32363  altxpsspw  32528  hfun  32729  ontgval  32869  ordtoplem  32873  ordcmp  32885  findreccl  32891  bj-xpnzex  33373  bj-snsetex  33378  topdifinfindis  33627  finxpreclem1  33659  ovoliunnfl  33875  volsupnfl  33878  heibor1lem  34030  heibor1  34031  lshpkrlem1  35066  lfl1dim  35077  leat3  35251  meetat2  35253  glbconxN  35334  pointpsubN  35707  pmapglbx  35725  linepsubclN  35907  dia2dimlem7  37026  dib1dim2  37124  diclspsn  37150  dih1dimatlem  37285  dihatexv2  37295  djhlsmcl  37370  hbtlem2  38371  hbtlem5  38375  rp-isfinite6  38539  snssiALTVD  39715  snssiALT  39716  elex2VD  39726  elex22VD  39727  fveqvfvv  41817  afv0fv0  41897  lswn0  42114  lidlmmgm  42594  1neven  42601  cznrng  42624  gsumpr  42808
  Copyright terms: Public domain W3C validator