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

Theorem eqeltri 2092
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 2085 . 2 (A 𝐶B 𝐶)
41, 3mpbir 134 1 A 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1228   wcel 1374
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-clel 2018
This theorem is referenced by:  eqeltrri  2093  3eltr4i  2101  intab  3618  inex2  3866  pwex  3906  ord3ex  3915  uniopel  3967  onsucelsucexmid  4199  elvvuni  4331  isarep2  4912  acexmidlemcase  5431  abrexex2  5674  oprabex  5678  oprabrexex2  5680  rdg0  5895  1on  5923  2on  5924  3on  5926  4on  5927  1onn  6004  2onn  6005  3onn  6006  4onn  6007  nqex  6222  nq0ex  6295  1pr  6404  ltexprlempr  6445  recexprlempr  6466  axcnex  6555  ax1cn  6557  ax1re  6558  bdinex2  7123  bj-inex  7130
  Copyright terms: Public domain W3C validator