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

Theorem eleq2i 2184
Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
eleq2i (𝐶𝐴𝐶𝐵)

Proof of Theorem eleq2i
StepHypRef Expression
1 eleq1i.1 . 2 𝐴 = 𝐵
2 eleq2 2181 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1316  wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eleq12i  2185  eleqtri  2192  eleq2s  2212  hbxfreq  2224  abeq2i  2228  abeq1i  2229  nfceqi  2254  raleqbii  2424  rexeqbii  2425  rabeq2i  2657  elab2g  2804  elrabf  2811  elrab3t  2812  elrab2  2816  cbvsbc  2909  elin2  3234  dfnul2  3335  noel  3337  rabn0m  3360  rabeq0  3362  eltpg  3539  tpid3g  3608  oprcl  3699  elunirab  3719  elintrab  3753  exss  4119  elop  4123  opm  4126  brabsb  4153  brabga  4156  pofun  4204  elsuci  4295  elsucg  4296  elsuc2g  4297  ordsucim  4386  peano2  4479  elxp  4526  brab2a  4562  brab2ga  4584  elco  4675  elcnv  4686  dmmrnm  4728  elrnmptg  4761  opelres  4794  rninxp  4952  funco  5133  elfv  5387  nfvres  5422  fvopab3g  5462  fvmptssdm  5473  fmptco  5554  funfvima  5617  fliftel  5662  acexmidlema  5733  acexmidlemb  5734  acexmidlem2  5739  eloprabga  5826  elrnmpo  5852  ovid  5855  offval  5957  xporderlem  6096  brtpos2  6116  issmo  6153  smores3  6158  tfrlem7  6182  tfrlem9  6184  tfr0dm  6187  tfri2  6231  rdgon  6251  freccllem  6267  frecfcllem  6269  frecsuclem  6271  el1o  6302  dif1o  6303  nnsucuniel  6359  elecg  6435  brecop  6487  erovlem  6489  oviec  6503  mapsncnv  6557  mptelixpg  6596  isfi  6623  enssdom  6624  map1  6674  xpcomco  6688  exmidpw  6770  fnfi  6793  fidcenumlemrks  6809  fidcenumlemrk  6810  djulclb  6908  eldju  6921  eldju2ndl  6925  eldju2ndr  6926  ctssdccl  6964  elni  7084  nlt1pig  7117  0nnq  7140  dfmq0qs  7205  dfplq0qs  7206  nqnq0  7217  elinp  7250  0npr  7259  ltdfpr  7282  nqprl  7327  nqpru  7328  addnqprlemfl  7335  addnqprlemfu  7336  mulnqprlemfl  7351  mulnqprlemfu  7352  cauappcvgprlemladdru  7432  suplocexprlemell  7489  addsrpr  7521  mulsrpr  7522  opelcn  7602  opelreal  7603  elreal  7604  elreal2  7606  0ncn  7607  addcnsr  7610  mulcnsr  7611  addvalex  7620  peano1nnnn  7628  peano2nnnn  7629  xrlenlt  7797  1nn  8699  peano2nn  8700  elnn0  8947  elnnne0  8959  un0addcl  8978  un0mulcl  8979  elxnn0  9010  uztrn2  9311  elnnuz  9330  elnn0uz  9331  elq  9382  elxr  9531  elfzm1b  9846  fz01or  9859  frecfzennn  10167  inftonninf  10182  seqf  10202  ser0  10255  ser0f  10256  hashinfom  10492  clim2ser  11074  clim2ser2  11075  isermulc2  11077  iserle  11079  climserle  11082  fsum3cvg3  11133  isumclim3  11160  isumadd  11168  sumsplitdc  11169  iserabs  11212  cvgcmpub  11213  isumshft  11227  isumsplit  11228  isumlessdc  11233  cvgratz  11269  cvgratgt0  11270  divides  11422  dvdsflip  11476  infssuzex  11569  ialgrlemconst  11651  ennnfonelemjn  11842  ennnfonelem1  11847  ennnfonelemdm  11860  istps  12126  lmss  12342  txuni2  12352  sinq34lt0t  12839  bdceq  12967  bj-nntrans  13076  bj-nnelirr  13078  ss1oel2o  13116  trilpolemisumle  13158
  Copyright terms: Public domain W3C validator