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

Theorem eqeltri 2126
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 2119 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 138 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1259  wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  eqeltrri  2127  3eltr4i  2135  intab  3672  inex2  3920  pwex  3960  ord3ex  3969  uniopel  4021  onsucelsucexmid  4283  elvvuni  4432  isarep2  5014  acexmidlemcase  5535  abrexex2  5779  oprabex  5783  oprabrexex2  5785  rdg0  6005  frecex  6012  1on  6039  2on  6040  3on  6042  4on  6043  1onn  6124  2onn  6125  3onn  6126  4onn  6127  nqex  6519  nq0ex  6596  1pr  6710  ltexprlempr  6764  recexprlempr  6788  cauappcvgprlemcl  6809  caucvgprlemcl  6832  caucvgprprlemcl  6860  addvalex  6978  peano1nnnn  6986  peano2nnnn  6987  axcnex  6993  ax1cn  6995  ax1re  6996  inelr  7649  cju  7989  2re  8060  3re  8064  4re  8067  5re  8069  6re  8071  7re  8073  8re  8075  9re  8077  2nn  8144  3nn  8145  4nn  8146  5nn  8147  6nn  8148  7nn  8149  8nn  8150  9nn  8151  nn0ex  8245  nneoor  8399  zeo  8402  deccl  8441  decnncl  8446  numnncl2  8449  decnncl2  8450  numsucc  8466  numma2c  8472  numadd  8473  numaddc  8474  nummul1c  8475  nummul2c  8476  pnfxr  8793  mnfxr  8795  xnegcl  8846  xrex  8857  ioof  8941  iseqex  9377  m1expcl2  9442  faccl  9603  facwordi  9608  faclbnd2  9610  bccl  9635  crre  9685  remim  9688  absval  9828  climle  10085  climcvg1nlem  10099  nn0o  10219  bdinex2  10407  bj-inex  10414
  Copyright terms: Public domain W3C validator