ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeltri Structured version   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  6422  1pr  6534  ltexprlempr  6581  recexprlempr  6603  cauappcvgprlemcl  6624  axcnex  6725  ax1cn  6727  ax1re  6728  inelr  7348  cju  7674  2re  7745  3re  7749  4re  7752  5re  7754  6re  7756  7re  7758  8re  7760  9re  7762  10re  7764  2nn  7835  3nn  7836  4nn  7837  5nn  7838  6nn  7839  7nn  7840  8nn  7841  9nn  7842  10nn  7843  nn0ex  7943  nneoor  8096  zeo  8099  decnncl  8136  deccl  8137  numnncl2  8140  decnncl2  8141  numsucc  8149  numma2c  8156  numadd  8157  numaddc  8158  nummul1c  8159  nummul2c  8160  pnfxr  8442  mnfxr  8444  xnegcl  8495  xrex  8506  ioof  8590  m1expcl2  8911  crre  9065  remim  9068  absval  9190  bdinex2  9331  bj-inex  9338
  Copyright terms: Public domain W3C validator