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

Theorem eleq1a 2908
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 2900 . 2 (𝐶 = 𝐴 → (𝐶𝐵𝐴𝐵))
21biimprcd 251 1 (𝐴𝐵 → (𝐶 = 𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893
This theorem is referenced by:  elex2  3517  elex22  3518  clel5OLD  3657  disjne  4402  eqoreldif  4616  ordelinel  6283  ssimaex  6742  fnex  6972  f1ocnv2d  7387  peano5  7593  mpoexw  7767  tfrlem8  8011  tz7.48-2  8069  tz7.49  8072  eroprf  8385  onfin  8698  pssnn  8725  ac6sfi  8751  elfiun  8883  brwdom  9020  ficardom  9379  ficard  9976  tskxpss  10183  inar1  10186  rankcf  10188  tskuni  10194  gruun  10217  nsmallnq  10388  prnmadd  10408  genpss  10415  eqlei  10739  eqlei2  10740  renegcli  10936  supaddc  11597  supadd  11598  supmul1  11599  supmullem2  11601  supmul  11602  nn0ind-raph  12071  uzwo  12300  iccid  12773  hashvnfin  13711  hashdifsnp1  13844  mertenslem2  15231  4sqlem1  16274  4sqlem4  16278  4sqlem11  16281  symggen  18529  psgnran  18574  odlem1  18594  gexlem1  18635  gsumpr  19006  lssvneln0  19654  lss1d  19666  lspsn  19705  lsmelval2  19788  psgnghm  20654  opnneiid  21664  cmpsublem  21937  metrest  23063  metustel  23089  dscopn  23112  ovolshftlem2  24040  subopnmbl  24134  deg1ldgn  24616  plyremlem  24822  coseq0negpitopi  25018  ppiublem1  25706  mptelee  26609  nbuhgr2vtx1edgblem  27061  numclwwlk1lem2foa  28061  shsleji  29075  spansnss  29276  spansncvi  29357  f1o3d  30301  sigaclcu2  31279  measdivcstALTV  31384  dfon2lem6  32931  noextendseq  33072  bdayfo  33080  scutf  33171  altxpsspw  33336  hfun  33537  ontgval  33677  ordtoplem  33681  ordcmp  33693  findreccl  33699  bj-xpnzex  34169  bj-snsetex  34173  bj-ismooredr2  34297  bj-ideqg1  34349  topdifinfindis  34510  finxpreclem1  34553  ovoliunnfl  34816  volsupnfl  34819  heibor1lem  34970  heibor1  34971  lshpkrlem1  36128  lfl1dim  36139  leat3  36313  meetat2  36315  glbconxN  36396  pointpsubN  36769  pmapglbx  36787  linepsubclN  36969  dia2dimlem7  38088  dib1dim2  38186  diclspsn  38212  dih1dimatlem  38347  dihatexv2  38357  djhlsmcl  38432  fltne  39152  3cubes  39167  hbtlem2  39604  hbtlem5  39608  rp-isfinite6  39764  snssiALTVD  41041  snssiALT  41042  elex2VD  41052  elex22VD  41053  fveqvfvv  43156  afv0fv0  43229  lswn0  43451  lidlmmgm  44094  1neven  44101  cznrng  44124
  Copyright terms: Public domain W3C validator