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

Theorem eleq1i 2498
Description: Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
eleq1i.1  |-  A  =  B
Assertion
Ref Expression
eleq1i  |-  ( A  e.  C  <->  B  e.  C )

Proof of Theorem eleq1i
StepHypRef Expression
1 eleq1i.1 . 2  |-  A  =  B
2 eleq1 2495 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
31, 2ax-mp 5 1  |-  ( A  e.  C  <->  B  e.  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    = wceq 1437    e. wcel 1872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-cleq 2414  df-clel 2417
This theorem is referenced by:  eleq12i  2500  eqeltri  2503  intexrab  4583  abssexg  4609  rmorabex  4681  xpsspw  4967  dfse2  5221  ordtri3or  5474  fressnfv  6093  fnotovb  6346  ovmpt2s  6434  snnex  6611  pwexb  6616  sucexb  6650  iprc  6742  f1stres  6829  f2ndres  6830  elxp6  6839  ottpos  6994  dftpos4  7003  tfr2b  7125  tz7.48-3  7172  difinf  7850  fiint  7857  infssuni  7874  fsuppunbi  7913  r1pwALT  8325  alephprc  8537  fin1a2lem12  8848  axcclem  8894  zorn2lem4  8936  zornn0g  8942  grothomex  9261  grothprimlem  9265  addclprlem2  9449  axicn  9581  pnfnre  9689  mnfnre  9690  0mnnnnn0  10909  swrdccatin12lem3  12848  swrdccat3  12850  swrdccat  12851  swrdccat3blem  12853  swrdccat3b  12854  harmonic  13916  nprmi  14638  prmrec  14865  issubm  16593  oppgsubm  17012  idrespermg  17051  issrg  17740  opprsubrg  18028  00lsp  18203  resubdrg  19174  cpmidpmat  19895  kgencn  20569  kgencn2  20570  txdis1cn  20648  qtopres  20711  qtopcn  20727  cfinfil  20906  tgphaus  21129  xmeterval  21445  blval2  21575  metuel2  21578  caucfil  22251  resscdrg  22323  finiunmbl  22495  iblre  22749  logno1  23579  rlimcnp2  23890  ppi2i  24094  nbgrasym  25165  nbgraf1olem3  25169  nbgraf1olem5  25171  nb3grapr  25179  nb3grapr2  25180  nb3gra2nb  25181  cusgra2v  25188  cusgra3v  25190  uvtxnbgra  25219  uvtxnb  25223  cusconngra  25402  2wlkonotv  25603  rusgrasn  25671  frisusgranb  25723  frgra3v  25728  3vfriswmgra  25731  1to3vfriendship  25734  2pthfrgrarn  25735  3cyclfrgrarn1  25738  4cycl2v2nb  25742  frgranbnb  25746  frgrancvvdeqlem2  25757  frgrancvvdeqlem4  25759  frgrancvvdeqlem7  25762  frgrawopreglem4  25773  frgrawopreg  25775  frgrawopreg2  25777  usg2spot2nb  25791  numclwwlkovf2ex  25812  avril1  25898  rngo1cl  26155  hhph  26829  nonbooli  27302  pjss2i  27331  atssma  28029  isrrext  28812  hasheuni  28914  dmvlsiga  28959  measiuns  29047  eulerpartlemmf  29216  rescon  29977  cvmlift2lem9  30042  rdgprc0  30447  bj-snsetex  31525  bj-tagex  31549  bj-pinftynrr  31628  bj-minftynrr  31632  poimirlem30  31934  ftc1anclem3  31983  ftc1anclem6  31986  rrnheibor  32133  isdrngo1  32159  islpln2ah  33083  lhpocnel2  33553  cdlemg31b0N  34230  cdlemg31b0a  34231  cdlemh  34353  cdlemk19w  34508  mzpclval  35536  wopprc  35855  dfac21  35894  binomcxplemdvsum  36674  binomcxp  36676  mccl  37618  stoweidlem17  37817  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem100  38010  omeiunltfirp  38248  hoidmvlelem5  38325  aovvdm  38557  aovvfunressn  38559  aovrcl  38561  aovvoveq  38564  aov0nbovbi  38567  fnotaovb  38570  pfxccat3  38837  pfxccat3a  38840  nbumgrel  39179  nbuhgr2vtx1edgb  39184  nbusgreledg  39185  nbusgrf1o0  39207  nb3grpr  39215  nb3grpr2  39216  nb3gr2nb  39217  uvtxumgrres  39237  cusgrsizeinds  39269  cusgrfi  39275  issubmgm  39408  zlmodzxzldeplem3  39916
  Copyright terms: Public domain W3C validator