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

Theorem eqeltrrid 2258
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
eqeltrrid.1 𝐵 = 𝐴
eqeltrrid.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqeltrrid (𝜑𝐴𝐶)

Proof of Theorem eqeltrrid
StepHypRef Expression
1 eqeltrrid.1 . . 3 𝐵 = 𝐴
21eqcomi 2174 . 2 𝐴 = 𝐵
3 eqeltrrid.2 . 2 (𝜑𝐵𝐶)
42, 3eqeltrid 2257 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348  wcel 2141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166
This theorem is referenced by:  dmrnssfld  4874  cnvexg  5148  opabbrex  5897  offval  6068  resfunexgALT  6087  abrexexg  6097  abrexex2g  6099  opabex3d  6100  oprssdmm  6150  unfidisj  6899  ssfii  6951  djuexb  7021  nqprlu  7509  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  mertenslem2  11499  exprmfct  12092  infpnlem1  12311  ennnfonelemg  12358  grpidvalg  12627  0opn  12798  difopn  12902  tgrest  12963  txbasex  13051  txdis1cn  13072  cnmptid  13075  cnmptc  13076  cnmpt1st  13082  cnmpt2nd  13083  cnmpt2c  13084  hmeoima  13104  hmeocld  13106  fsumcncntop  13350
  Copyright terms: Public domain W3C validator