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

Theorem eleq1i 2830
Description: Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
eleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
eleq1i (𝐴𝐶𝐵𝐶)

Proof of Theorem eleq1i
StepHypRef Expression
1 eleq1i.1 . 2 𝐴 = 𝐵
2 eleq1 2827 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1539  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817
This theorem is referenced by:  eleq12i  2832  eqneltri  2833  eqeltri  2836  intexrab  5265  abssexg  5306  rmorabex  5376  xpsspw  5721  dfse2  6011  dfse3  6243  ordtri3or  6302  fressnfv  7041  fnotovb  7334  ovmpos  7430  abnex  7616  sucexb  7663  f1stres  7864  f2ndres  7865  elxp6  7874  ottpos  8061  dftpos4  8070  tfr2b  8236  tz7.48-3  8284  unfi  8964  difinf  9093  fiint  9100  infssuni  9119  fsuppunbi  9158  r1pwALT  9613  djuexb  9676  alephprc  9864  fin1a2lem12  10176  axcclem  10222  zorn2lem4  10264  zornn0g  10270  grothomex  10594  grothprimlem  10598  addclprlem2  10782  axicn  10915  0mnnnnn0  12274  frnnn0fsupp  12299  pfxccatin12lem3  14454  pfxccat3  14456  swrdccat  14457  pfxccat3a  14460  swrdccat3blem  14461  swrdccat3b  14462  harmonic  15580  nprmi  16403  issubm  18451  idresefmnd  18547  mulgfval  18711  oppgsubm  18978  idrespermg  19028  issrg  19752  srgfcl  19760  opprsubrg  20054  resubdrg  20822  cpmidpmat  22031  kgencn  22716  kgencn2  22717  txdis1cn  22795  qtopres  22858  qtopcn  22874  cfinfil  23053  tgphaus  23277  xmeterval  23594  blval2  23727  metuel2  23730  iscvsp  24300  zclmncvs  24321  caucfil  24456  resscdrg  24531  finiunmbl  24717  iblre  24967  logno1  25800  rlimcnp2  26125  ppi2i  26327  gausslemma2dlem1a  26522  2lgslem4  26563  usgredgffibi  27700  nbupgrel  27721  nbuhgr2vtx1edgb  27728  nbusgreledg  27729  nbusgrf1o0  27745  nb3grpr  27758  nb3grpr2  27759  nb3gr2nb  27760  cusgrsizeinds  27828  cusgrfi  27834  finsumvtxdg2size  27926  wlkp1lem1  28050  wlkp1lem7  28056  wlkp1lem8  28057  wwlks2onsym  28332  rusgrnumwwlks  28348  clwwlknclwwlkdifnum  28353  clwwlknonfin  28467  clwwlknonex2  28482  umgr3cyclex  28556  eupthp1  28589  eupth2eucrct  28590  frcond3  28642  frgr3v  28648  3vfriswmgr  28651  1to3vfriendship  28654  2pthfrgrrn  28655  3cyclfrgrrn1  28658  4cycl2v2nb  28662  frgrnbnb  28666  frgrncvvdeqlem3  28674  frgrncvvdeqlem6  28677  frgrhash2wsp  28705  fusgr2wsp2nb  28707  numclwwlk1  28734  avril1  28836  n0lplig  28854  hhph  29549  nonbooli  30022  pjss2i  30051  atssma  30749  isrrext  31959  hasheuni  32062  dmvlsiga  32106  measiuns  32194  eulerpartlemmf  32351  fineqvrep  33073  cusgr3cyclex  33107  resconn  33217  cvmlift2lem9  33282  rdgprc0  33778  noxp1o  33875  bj-snsetex  35162  bj-tagex  35186  bj-0int  35281  poimirlem30  35816  ftc1anclem3  35861  ftc1anclem6  35864  rrnheibor  36004  rngo1cl  36106  isdrngo1  36123  dfcoeleqvrels  36741  islpln2ah  37570  lhpocnel2  38040  cdlemg31b0N  38715  cdlemg31b0a  38716  cdlemh  38838  cdlemk19w  38993  aks4d1lem1  40077  sticksstones4  40112  mzpclval  40554  wopprc  40859  dfac21  40898  sucomisnotcard  41158  binomcxplemdvsum  41980  binomcxp  41982  mccl  43146  fprodcn  43148  stoweidlem17  43565  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem100  43754  omeiunltfirp  44064  hoidmvlelem5  44144  issmf  44273  issmff  44279  smflimlem4  44319  smflim  44322  smflim2  44350  smflimsuplem1  44364  smflimsuplem8  44371  smflimsup  44372  aiotaexb  44592  aiotavb  44593  aovvdm  44688  aovvfunressn  44690  aovrcl  44692  aovvoveq  44695  aov0nbovbi  44698  fnotaovb  44701  prmdvdsfmtnof1lem1  45047  341fppr2  45197  9fppr8  45200  issubmgm  45354  zlmodzxzldeplem3  45854  itscnhlinecirc02p  46142
  Copyright terms: Public domain W3C validator