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

Theorem eqeltri 2157
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 2150 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 144 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1287  wcel 1436
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  eqeltrri  2158  3eltr4i  2166  intab  3700  inex2  3948  vpwex  3988  ord3ex  3998  uniopel  4056  onsucelsucexmid  4318  elvvuni  4469  isarep2  5063  acexmidlemcase  5602  abrexex2  5846  oprabex  5850  oprabrexex2  5852  rdg0  6100  frecex  6107  1on  6136  2on  6138  3on  6140  4on  6141  1onn  6225  2onn  6226  3onn  6227  4onn  6228  mapsnf1o2  6399  exmidpw  6570  unfiexmid  6574  xpfi  6584  ssfirab  6587  fnfi  6590  sbthlemi10  6612  nqex  6859  nq0ex  6936  1pr  7050  ltexprlempr  7104  recexprlempr  7128  cauappcvgprlemcl  7149  caucvgprlemcl  7172  caucvgprprlemcl  7200  addvalex  7318  peano1nnnn  7326  peano2nnnn  7327  axcnex  7333  ax1cn  7335  ax1re  7336  pnfxr  7477  mnfxr  7481  inelr  7995  cju  8349  2re  8420  3re  8424  4re  8427  5re  8429  6re  8431  7re  8433  8re  8435  9re  8437  2nn  8504  3nn  8505  4nn  8506  5nn  8507  6nn  8508  7nn  8509  8nn  8510  9nn  8511  nn0ex  8605  nneoor  8774  zeo  8777  deccl  8816  decnncl  8821  numnncl2  8824  decnncl2  8825  numsucc  8841  numma2c  8847  numadd  8848  numaddc  8849  nummul1c  8850  nummul2c  8851  xnegcl  9219  xrex  9230  ioof  9314  iseqex  9774  m1expcl2  9868  faccl  10032  facwordi  10037  faclbnd2  10039  bccl  10064  crre  10179  remim  10182  absval  10322  climle  10607  climcvg1nlem  10621  nn0o  10774  bdinex2  11221  bj-inex  11228  nnpredcl  11320  peano3nninf  11327  nninfex  11331
  Copyright terms: Public domain W3C validator