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

Theorem eleq2i 2206
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 2203 . 2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
31, 2ax-mp 5 1  |-  ( C  e.  A  <->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1331    e. wcel 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  eleq12i  2207  eleqtri  2214  eleq2s  2234  hbxfreq  2246  abeq2i  2250  abeq1i  2251  nfceqi  2277  raleqbii  2447  rexeqbii  2448  rabeq2i  2683  elab2g  2831  elrabf  2838  elrab3t  2839  elrab2  2843  cbvsbcw  2936  cbvsbc  2937  elin2  3264  dfnul2  3365  noel  3367  rabn0m  3390  rabeq0  3392  eltpg  3569  tpid3g  3638  oprcl  3729  elunirab  3749  elintrab  3783  exss  4149  elop  4153  opm  4156  brabsb  4183  brabga  4186  pofun  4234  elsuci  4325  elsucg  4326  elsuc2g  4327  ordsucim  4416  peano2  4509  elxp  4556  brab2a  4592  brab2ga  4614  elco  4705  elcnv  4716  dmmrnm  4758  elrnmptg  4791  opelres  4824  rninxp  4982  funco  5163  elfv  5419  nfvres  5454  fvopab3g  5494  fvmptssdm  5505  fmptco  5586  funfvima  5649  fliftel  5694  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  eloprabga  5858  elrnmpo  5884  ovid  5887  offval  5989  xporderlem  6128  brtpos2  6148  issmo  6185  smores3  6190  tfrlem7  6214  tfrlem9  6216  tfr0dm  6219  tfri2  6263  rdgon  6283  freccllem  6299  frecfcllem  6301  frecsuclem  6303  el1o  6334  dif1o  6335  nnsucuniel  6391  elecg  6467  brecop  6519  erovlem  6521  oviec  6535  mapsncnv  6589  mptelixpg  6628  isfi  6655  enssdom  6656  map1  6706  xpcomco  6720  exmidpw  6802  fnfi  6825  fidcenumlemrks  6841  fidcenumlemrk  6842  djulclb  6940  eldju  6953  eldju2ndl  6957  eldju2ndr  6958  ctssdccl  6996  elni  7128  nlt1pig  7161  0nnq  7184  dfmq0qs  7249  dfplq0qs  7250  nqnq0  7261  elinp  7294  0npr  7303  ltdfpr  7326  nqprl  7371  nqpru  7372  addnqprlemfl  7379  addnqprlemfu  7380  mulnqprlemfl  7395  mulnqprlemfu  7396  cauappcvgprlemladdru  7476  suplocexprlemell  7533  addsrpr  7565  mulsrpr  7566  opelcn  7646  opelreal  7647  elreal  7648  elreal2  7650  0ncn  7651  addcnsr  7654  mulcnsr  7655  addvalex  7664  peano1nnnn  7672  peano2nnnn  7673  xrlenlt  7841  1nn  8743  peano2nn  8744  elnn0  8991  elnnne0  9003  un0addcl  9022  un0mulcl  9023  elxnn0  9054  uztrn2  9355  elnnuz  9374  elnn0uz  9375  elq  9426  elxr  9575  elfzm1b  9890  fz01or  9903  frecfzennn  10211  inftonninf  10226  seqf  10246  ser0  10299  ser0f  10300  hashinfom  10536  clim2ser  11118  clim2ser2  11119  isermulc2  11121  iserle  11123  climserle  11126  fsum3cvg3  11177  isumclim3  11204  isumadd  11212  sumsplitdc  11213  iserabs  11256  cvgcmpub  11257  isumshft  11271  isumsplit  11272  isumlessdc  11277  cvgratz  11313  cvgratgt0  11314  clim2prod  11320  clim2divap  11321  prodf1  11323  divides  11506  dvdsflip  11560  infssuzex  11653  ialgrlemconst  11735  ennnfonelemjn  11926  ennnfonelem1  11931  ennnfonelemdm  11944  istps  12213  lmss  12429  txuni2  12439  sinq34lt0t  12934  bdceq  13099  bj-nntrans  13208  bj-nnelirr  13210  ss1oel2o  13248  trilpolemisumle  13292
  Copyright terms: Public domain W3C validator