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

Theorem eqeltri 2110
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltr.1 𝐴 = 𝐵
eqeltr.2 𝐵𝐶
Assertion
Ref Expression
eqeltri 𝐴𝐶

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltr.2 . 2 𝐵𝐶
2 eqeltr.1 . . 3 𝐴 = 𝐵
32eleq1i 2103 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 134 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1243  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:  eqeltrri  2111  3eltr4i  2119  intab  3644  inex2  3892  pwex  3932  ord3ex  3941  uniopel  3993  onsucelsucexmid  4255  elvvuni  4404  isarep2  4986  acexmidlemcase  5507  abrexex2  5751  oprabex  5755  oprabrexex2  5757  rdg0  5974  frecex  5981  1on  6008  2on  6009  3on  6011  4on  6012  1onn  6093  2onn  6094  3onn  6095  4onn  6096  nqex  6459  nq0ex  6536  1pr  6650  ltexprlempr  6704  recexprlempr  6728  cauappcvgprlemcl  6749  caucvgprlemcl  6772  caucvgprprlemcl  6800  addvalex  6918  peano1nnnn  6926  peano2nnnn  6927  axcnex  6933  ax1cn  6935  ax1re  6936  inelr  7573  cju  7911  2re  7983  3re  7987  4re  7990  5re  7992  6re  7994  7re  7996  8re  7998  9re  8000  10re  8002  2nn  8075  3nn  8076  4nn  8077  5nn  8078  6nn  8079  7nn  8080  8nn  8081  9nn  8082  10nn  8083  nn0ex  8185  nneoor  8338  zeo  8341  decnncl  8378  deccl  8379  numnncl2  8382  decnncl2  8383  numsucc  8391  numma2c  8398  numadd  8399  numaddc  8400  nummul1c  8401  nummul2c  8402  pnfxr  8690  mnfxr  8692  xnegcl  8743  xrex  8754  ioof  8838  iseqex  9187  m1expcl2  9251  crre  9431  remim  9434  absval  9573  climle  9828  climcvg1nlem  9842  bdinex2  9994  bj-inex  10001
  Copyright terms: Public domain W3C validator