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

Theorem eqeltri 2160
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 2153 . 2  |-  ( A  e.  C  <->  B  e.  C )
41, 3mpbir 144 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1289    e. wcel 1438
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  eqeltrri  2161  3eltr4i  2169  intab  3712  inex2  3966  vpwex  4006  ord3ex  4016  uniopel  4074  onsucelsucexmid  4336  elvvuni  4490  isarep2  5087  acexmidlemcase  5629  abrexex2  5877  oprabex  5881  oprabrexex2  5883  rdg0  6134  frecex  6141  1on  6170  2on  6172  3on  6174  4on  6175  1onn  6259  2onn  6260  3onn  6261  4onn  6262  mapsnf1o2  6433  exmidpw  6604  unfiexmid  6608  xpfi  6619  ssfirab  6622  fnfi  6625  iunfidisj  6634  fidcenumlemr  6643  sbthlemi10  6654  nqex  6901  nq0ex  6978  1pr  7092  ltexprlempr  7146  recexprlempr  7170  cauappcvgprlemcl  7191  caucvgprlemcl  7214  caucvgprprlemcl  7242  addvalex  7360  peano1nnnn  7368  peano2nnnn  7369  axcnex  7375  ax1cn  7377  ax1re  7378  pnfxr  7519  mnfxr  7523  inelr  8037  cju  8393  2re  8463  3re  8467  4re  8470  5re  8472  6re  8474  7re  8476  8re  8478  9re  8480  2nn  8547  3nn  8548  4nn  8549  5nn  8550  6nn  8551  7nn  8552  8nn  8553  9nn  8554  nn0ex  8649  nneoor  8818  zeo  8821  deccl  8860  decnncl  8865  numnncl2  8868  decnncl2  8869  numsucc  8885  numma2c  8891  numadd  8892  numaddc  8893  nummul1c  8894  nummul2c  8895  xnegcl  9263  xrex  9274  ioof  9358  iseqex  9821  seqex  9822  m1expcl2  9942  faccl  10108  facwordi  10113  faclbnd2  10115  bccl  10140  crre  10256  remim  10259  absval  10399  climle  10686  climcvg1nlem  10702  geo2lim  10871  nn0o  11000  bdinex2  11448  bj-inex  11455  nnpredcl  11547  peano3nninf  11554  nninfex  11558
  Copyright terms: Public domain W3C validator