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

Theorem eqeltri 2152
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltr.1  |-  A  =  B
eqeltr.2  |-  B  e.  C
Assertion
Ref Expression
eqeltri  |-  A  e.  C

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltr.2 . 2  |-  B  e.  C
2 eqeltr.1 . . 3  |-  A  =  B
32eleq1i 2145 . 2  |-  ( A  e.  C  <->  B  e.  C )
41, 3mpbir 144 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1285    e. wcel 1434
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  eqeltrri  2153  3eltr4i  2161  intab  3673  inex2  3921  pwex  3961  ord3ex  3969  uniopel  4019  onsucelsucexmid  4281  elvvuni  4430  isarep2  5017  acexmidlemcase  5538  abrexex2  5782  oprabex  5786  oprabrexex2  5788  rdg0  6036  frecex  6043  1on  6072  2on  6073  3on  6075  4on  6076  1onn  6159  2onn  6160  3onn  6161  4onn  6162  unfiexmid  6438  fnfi  6446  nqex  6615  nq0ex  6692  1pr  6806  ltexprlempr  6860  recexprlempr  6884  cauappcvgprlemcl  6905  caucvgprlemcl  6928  caucvgprprlemcl  6956  addvalex  7074  peano1nnnn  7082  peano2nnnn  7083  axcnex  7089  ax1cn  7091  ax1re  7092  pnfxr  7233  mnfxr  7237  inelr  7751  cju  8105  2re  8176  3re  8180  4re  8183  5re  8185  6re  8187  7re  8189  8re  8191  9re  8193  2nn  8260  3nn  8261  4nn  8262  5nn  8263  6nn  8264  7nn  8265  8nn  8266  9nn  8267  nn0ex  8361  nneoor  8530  zeo  8533  deccl  8572  decnncl  8577  numnncl2  8580  decnncl2  8581  numsucc  8597  numma2c  8603  numadd  8604  numaddc  8605  nummul1c  8606  nummul2c  8607  xnegcl  8975  xrex  8986  ioof  9070  iseqex  9523  m1expcl2  9595  faccl  9759  facwordi  9764  faclbnd2  9766  bccl  9791  crre  9882  remim  9885  absval  10025  climle  10310  climcvg1nlem  10324  nn0o  10451  bdinex2  10849  bj-inex  10856
  Copyright terms: Public domain W3C validator