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

Theorem eleq1i 2721
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 2718 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  eleq12i  2723  eqeltri  2726  intexrab  4853  abssexg  4881  rmorabex  4958  xpsspw  5266  dfse2  5534  ordtri3or  5793  fressnfv  6467  fnotovb  6735  fnotovbOLD  6736  ovmpt2s  6826  abnex  7007  snnexOLD  7009  sucexb  7051  iprc  7143  f1stres  7234  f2ndres  7235  elxp6  7244  ottpos  7407  dftpos4  7416  tfr2b  7537  tz7.48-3  7584  difinf  8271  fiint  8278  infssuni  8298  fsuppunbi  8337  r1pwALT  8747  alephprc  8960  fin1a2lem12  9271  axcclem  9317  zorn2lem4  9359  zornn0g  9365  grothomex  9689  grothprimlem  9693  addclprlem2  9877  axicn  10009  pnfnre  10119  mnfnre  10120  0mnnnnn0  11363  swrdccatin12lem3  13536  swrdccat3  13538  swrdccat  13539  swrdccat3blem  13541  swrdccat3b  13542  harmonic  14635  nprmi  15449  prmrec  15673  issubm  17394  oppgsubm  17838  idrespermg  17877  issrg  18553  srgfcl  18561  opprsubrg  18849  00lsp  19029  resubdrg  20002  cpmidpmat  20726  kgencn  21407  kgencn2  21408  txdis1cn  21486  qtopres  21549  qtopcn  21565  cfinfil  21744  tgphaus  21967  xmeterval  22284  blval2  22414  metuel2  22417  iscvsp  22974  zclmncvs  22994  caucfil  23127  resscdrg  23200  finiunmbl  23358  iblre  23605  logno1  24427  rlimcnp2  24738  ppi2i  24940  gausslemma2dlem1a  25135  2lgslem4  25176  usgredgffibi  26261  nbupgrel  26286  nbuhgr2vtx1edgb  26293  nbusgreledg  26294  nbusgrf1o0  26315  nb3grpr  26328  nb3grpr2  26329  nb3gr2nb  26330  cusgrsizeinds  26404  cusgrfi  26410  finsumvtxdg2size  26502  wlkp1lem1  26626  wlkp1lem7  26632  wlkp1lem8  26633  wwlks2onsym  26924  rusgrnumwwlks  26941  clwwlknclwwlkdifnum  26946  clwwlknclwwlkdifnumOLD  26948  clwwlknonfin  27069  clwwlknonex2  27084  umgr3cyclex  27161  eupthp1  27194  eupth2eucrct  27195  frcond3  27249  frgr3v  27255  3vfriswmgr  27258  1to3vfriendship  27261  2pthfrgrrn  27262  3cyclfrgrrn1  27265  4cycl2v2nb  27269  frgrnbnb  27273  frgrncvvdeqlem3  27281  frgrncvvdeqlem6  27284  frgrhash2wsp  27312  fusgr2wsp2nb  27314  numclwwlk1  27351  avril1  27449  n0lplig  27465  hhph  28163  nonbooli  28638  pjss2i  28667  atssma  29365  isrrext  30172  hasheuni  30275  dmvlsiga  30320  measiuns  30408  eulerpartlemmf  30565  resconn  31354  cvmlift2lem9  31419  rdgprc0  31823  noxp1o  31941  bj-snsetex  33076  bj-tagex  33100  bj-0int  33180  bj-pinftynrr  33239  bj-minftynrr  33243  poimirlem30  33569  ftc1anclem3  33617  ftc1anclem6  33620  rrnheibor  33766  rngo1cl  33868  isdrngo1  33885  islpln2ah  35153  lhpocnel2  35623  cdlemg31b0N  36299  cdlemg31b0a  36300  cdlemh  36422  cdlemk19w  36577  mzpclval  37605  wopprc  37914  dfac21  37953  binomcxplemdvsum  38871  binomcxp  38873  eqneltri  39560  mccl  40148  fprodcn  40150  stoweidlem17  40552  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem100  40741  omeiunltfirp  41054  hoidmvlelem5  41134  issmf  41258  issmff  41264  smflimlem4  41303  smflim  41306  smflim2  41333  smflimsuplem1  41347  smflimsuplem8  41354  smflimsup  41355  aovvdm  41586  aovvfunressn  41588  aovrcl  41590  aovvoveq  41593  aov0nbovbi  41596  fnotaovb  41599  pfxccat3  41751  pfxccat3a  41754  prmdvdsfmtnof1lem1  41821  issubmgm  42114  zlmodzxzldeplem3  42616
  Copyright terms: Public domain W3C validator