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

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

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltr.2 . 2 B 𝐶
2 eqeltr.1 . . 3 A = B
32eleq1i 2100 . 2 (A 𝐶B 𝐶)
41, 3mpbir 134 1 A 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1242   wcel 1390
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033
This theorem is referenced by:  eqeltrri  2108  3eltr4i  2116  intab  3635  inex2  3883  pwex  3923  ord3ex  3932  uniopel  3984  onsucelsucexmid  4215  elvvuni  4347  isarep2  4929  acexmidlemcase  5450  abrexex2  5693  oprabex  5697  oprabrexex2  5699  rdg0  5914  1on  5947  2on  5948  3on  5950  4on  5951  1onn  6029  2onn  6030  3onn  6031  4onn  6032  nqex  6347  nq0ex  6423  1pr  6535  ltexprlempr  6582  recexprlempr  6604  cauappcvgprlemcl  6625  caucvgprlemcl  6647  axcnex  6745  ax1cn  6747  ax1re  6748  inelr  7368  cju  7694  2re  7765  3re  7769  4re  7772  5re  7774  6re  7776  7re  7778  8re  7780  9re  7782  10re  7784  2nn  7855  3nn  7856  4nn  7857  5nn  7858  6nn  7859  7nn  7860  8nn  7861  9nn  7862  10nn  7863  nn0ex  7963  nneoor  8116  zeo  8119  decnncl  8156  deccl  8157  numnncl2  8160  decnncl2  8161  numsucc  8169  numma2c  8176  numadd  8177  numaddc  8178  nummul1c  8179  nummul2c  8180  pnfxr  8462  mnfxr  8464  xnegcl  8515  xrex  8526  ioof  8610  m1expcl2  8931  crre  9085  remim  9088  absval  9210  bdinex2  9355  bj-inex  9362
  Copyright terms: Public domain W3C validator