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  6580  recexprlempr  6602  axcnex  6705  ax1cn  6707  ax1re  6708  inelr  7328  cju  7654  2re  7725  3re  7729  4re  7732  5re  7734  6re  7736  7re  7738  8re  7740  9re  7742  10re  7744  2nn  7815  3nn  7816  4nn  7817  5nn  7818  6nn  7819  7nn  7820  8nn  7821  9nn  7822  10nn  7823  nn0ex  7923  nneoor  8076  zeo  8079  decnncl  8116  deccl  8117  numnncl2  8120  decnncl2  8121  numsucc  8129  numma2c  8136  numadd  8137  numaddc  8138  nummul1c  8139  nummul2c  8140  pnfxr  8422  mnfxr  8424  xnegcl  8475  xrex  8486  ioof  8570  m1expcl2  8891  crre  9045  remim  9048  bdinex2  9285  bj-inex  9292
  Copyright terms: Public domain W3C validator