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

Theorem eleq1a 2906
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 2898 . 2 (𝐶 = 𝐴 → (𝐶𝐵𝐴𝐵))
21biimprcd 252 1 (𝐴𝐵 → (𝐶 = 𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-clel 2891
This theorem is referenced by:  elex2  3515  elex22  3516  clel5OLD  3656  disjne  4402  eqoreldif  4614  ordelinel  6282  ssimaex  6741  fnex  6972  f1ocnv2d  7390  peano5  7597  mpoexw  7768  tfrlem8  8012  tz7.48-2  8070  tz7.49  8073  eroprf  8387  onfin  8701  pssnn  8728  ac6sfi  8754  elfiun  8886  brwdom  9023  ficardom  9382  ficard  9979  tskxpss  10186  inar1  10189  rankcf  10191  tskuni  10197  gruun  10220  nsmallnq  10391  prnmadd  10411  genpss  10418  eqlei  10742  eqlei2  10743  renegcli  10939  supaddc  11600  supadd  11601  supmul1  11602  supmullem2  11604  supmul  11605  nn0ind-raph  12074  uzwo  12303  iccid  12775  hashvnfin  13713  hashdifsnp1  13846  mertenslem2  15233  4sqlem1  16276  4sqlem4  16280  4sqlem11  16283  symggen  18590  psgnran  18635  odlem1  18655  gexlem1  18696  gsumpr  19067  lssvneln0  19715  lss1d  19727  lspsn  19766  lsmelval2  19849  psgnghm  20716  opnneiid  21726  cmpsublem  21999  metrest  23126  metustel  23152  dscopn  23175  ovolshftlem2  24103  subopnmbl  24197  deg1ldgn  24679  plyremlem  24885  coseq0negpitopi  25081  ppiublem1  25770  mptelee  26673  nbuhgr2vtx1edgblem  27125  numclwwlk1lem2foa  28125  shsleji  29139  spansnss  29340  spansncvi  29421  f1o3d  30364  sigaclcu2  31367  measdivcstALTV  31472  dfon2lem6  33021  noextendseq  33162  bdayfo  33170  scutf  33261  altxpsspw  33426  hfun  33627  ontgval  33767  ordtoplem  33771  ordcmp  33783  findreccl  33789  bj-xpnzex  34259  bj-snsetex  34263  bj-ismooredr2  34389  bj-ideqg1  34443  topdifinfindis  34614  finxpreclem1  34657  ovoliunnfl  34921  volsupnfl  34924  heibor1lem  35074  heibor1  35075  lshpkrlem1  36233  lfl1dim  36244  leat3  36418  meetat2  36420  glbconxN  36501  pointpsubN  36874  pmapglbx  36892  linepsubclN  37074  dia2dimlem7  38193  dib1dim2  38291  diclspsn  38317  dih1dimatlem  38452  dihatexv2  38462  djhlsmcl  38537  fltne  39257  3cubes  39272  hbtlem2  39709  hbtlem5  39713  rp-isfinite6  39869  snssiALTVD  41146  snssiALT  41147  elex2VD  41157  elex22VD  41158  fveqvfvv  43260  afv0fv0  43333  lswn0  43589  lidlmmgm  44181  1neven  44188  cznrng  44211
  Copyright terms: Public domain W3C validator