ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleq2i Unicode version

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

Proof of Theorem eleq2i
StepHypRef Expression
1 eleq1i.1 . 2  |-  A  =  B
2 eleq2 2146 . 2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
31, 2ax-mp 7 1  |-  ( C  e.  A  <->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 103    = wceq 1285    e. wcel 1434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-clel 2079
This theorem is referenced by:  eleq12i  2150  eleqtri  2157  eleq2s  2177  hbxfreq  2189  abeq2i  2193  abeq1i  2194  nfceqi  2219  raleqbii  2383  rexeqbii  2384  rabeq2i  2607  elab2g  2748  elrabf  2755  elrab3t  2756  elrab2  2760  cbvsbc  2851  elin2  3170  dfnul2  3269  noel  3271  rabn0m  3288  rabeq0  3290  eltpg  3456  tpid3g  3523  oprcl  3614  elunirab  3634  elintrab  3668  exss  4010  elop  4014  opm  4017  brabsb  4044  brabga  4047  pofun  4095  elsuci  4186  elsucg  4187  elsuc2g  4188  ordsucim  4272  peano2  4364  elxp  4408  brab2a  4439  brab2ga  4461  elcnv  4560  dmmrnm  4602  elrnmptg  4634  opelres  4665  rninxp  4814  funco  4990  elfv  5228  nfvres  5259  fvopab3g  5298  fvmptssdm  5308  fmptco  5383  funfvima  5443  fliftel  5485  acexmidlema  5555  acexmidlemb  5556  acexmidlem2  5561  eloprabga  5643  elrnmpt2  5666  ovid  5669  offval  5771  xporderlem  5904  brtpos2  5921  issmo  5958  smores3  5963  tfrlem7  5987  tfrlem9  5989  tfr0dm  5992  tfri2  6036  rdgon  6056  freccllem  6072  frecfcllem  6074  frecsuclem  6076  el1o  6105  dif1o  6106  nnsucuniel  6160  elecg  6232  brecop  6284  erovlem  6286  oviec  6300  isfi  6330  enssdom  6331  xpcomco  6392  fnfi  6479  djur  6563  eldju2ndl  6566  eldju2ndr  6567  elni  6630  nlt1pig  6663  0nnq  6686  dfmq0qs  6751  dfplq0qs  6752  nqnq0  6763  elinp  6796  0npr  6805  ltdfpr  6828  nqprl  6873  nqpru  6874  addnqprlemfl  6881  addnqprlemfu  6882  mulnqprlemfl  6897  mulnqprlemfu  6898  cauappcvgprlemladdru  6978  addsrpr  7054  mulsrpr  7055  opelcn  7127  opelreal  7128  elreal  7129  elreal2  7131  0ncn  7132  addcnsr  7134  mulcnsr  7135  addvalex  7144  peano1nnnn  7152  peano2nnnn  7153  xrlenlt  7314  1nn  8187  peano2nn  8188  elnn0  8427  elnnne0  8439  un0addcl  8458  un0mulcl  8459  elxnn0  8490  uztrn2  8787  elnnuz  8806  elnn0uz  8807  elq  8858  elxr  8998  elfzm1b  9261  fz01or  9274  frecfzennn  9578  iseqfcl  9605  iseqfclt  9606  iser0  9638  iser0f  9639  hashinfom  9872  clim2iser  10394  clim2iser2  10395  iisermulc2  10397  iserile  10399  climserile  10402  divides  10423  dvdsflip  10477  infssuzex  10570  ialgrlemconst  10650  ialgrf  10652  bdceq  10918  bj-nntrans  11031  bj-nnelirr  11033
  Copyright terms: Public domain W3C validator