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

Theorem eleq2i 2104
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 2101 . 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 98    = wceq 1243    e. wcel 1393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036
This theorem is referenced by:  eleq12i  2105  eleqtri  2112  eleq2s  2132  hbxfreq  2144  abeq2i  2148  abeq1i  2149  nfceqi  2174  raleqbii  2333  rexeqbii  2334  rabeq2i  2551  elab2g  2686  elrabf  2693  elrab3t  2694  elrab2  2697  cbvsbc  2788  elin2  3124  dfnul2  3223  noel  3225  rabn0m  3242  rabeq0  3244  eltpg  3413  tpid3g  3480  oprcl  3570  elunirab  3590  elintrab  3624  exss  3960  elop  3965  opm  3968  brabsb  3995  brabga  3998  pofun  4046  elsuci  4127  elsucg  4128  elsuc2g  4129  ordsucim  4213  peano2  4296  elxp  4340  brab2a  4371  brab2ga  4393  elcnv  4490  dmmrnm  4532  elrnmptg  4564  opelres  4595  rninxp  4742  funco  4918  elfv  5154  nfvres  5184  fvopab3g  5223  fvmptssdm  5233  fmptco  5308  funfvima  5368  fliftel  5411  acexmidlema  5481  acexmidlemb  5482  acexmidlem2  5487  eloprabga  5569  elrnmpt2  5592  ovid  5595  offval  5697  xporderlem  5830  brtpos2  5844  issmo  5881  smores3  5886  tfrlem7  5911  tfrlem9  5913  tfr0  5915  tfri2  5930  el1o  5998  dif1o  5999  elecg  6122  brecop  6174  erovlem  6176  oviec  6190  isfi  6219  enssdom  6220  xpcomco  6278  elni  6378  nlt1pig  6411  0nnq  6434  dfmq0qs  6499  dfplq0qs  6500  nqnq0  6511  elinp  6544  0npr  6553  ltdfpr  6576  nqprl  6621  nqpru  6622  addnqprlemfl  6629  addnqprlemfu  6630  mulnqprlemfl  6645  mulnqprlemfu  6646  cauappcvgprlemladdru  6726  addsrpr  6802  mulsrpr  6803  opelcn  6875  opelreal  6876  elreal  6877  elreal2  6879  0ncn  6880  addcnsr  6882  mulcnsr  6883  addvalex  6892  peano1nnnn  6900  peano2nnnn  6901  xrlenlt  7055  1nn  7892  peano2nn  7893  elnn0  8146  elnnne0  8158  un0addcl  8178  un0mulcl  8179  uztrn2  8453  elnnuz  8472  elnn0uz  8473  elq  8520  elxr  8654  elfzm1b  8918  frecfzennn  9072  iseqf  9093  iser0  9119  iser0f  9120  clim2iser  9725  clim2iser2  9726  iisermulc2  9728  iserile  9730  climserile  9733  ialgrlemconst  9750  ialgrf  9752  bdceq  9826  bj-nntrans  9940  bj-nnelirr  9942
  Copyright terms: Public domain W3C validator