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

Theorem eqeltrrid 2245
 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 2161 . 2
3 eqeltrrid.2 . 2
42, 3eqeltrid 2244 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1335   wcel 2128 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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153 This theorem is referenced by:  dmrnssfld  4846  cnvexg  5120  opabbrex  5859  offval  6033  resfunexgALT  6052  abrexexg  6060  abrexex2g  6062  opabex3d  6063  oprssdmm  6113  unfidisj  6859  ssfii  6911  djuexb  6978  nqprlu  7450  iccshftr  9880  iccshftl  9882  iccdil  9884  icccntr  9886  mertenslem2  11415  exprmfct  11994  ennnfonelemg  12104  0opn  12364  difopn  12468  tgrest  12529  txbasex  12617  txdis1cn  12638  cnmptid  12641  cnmptc  12642  cnmpt1st  12648  cnmpt2nd  12649  cnmpt2c  12650  hmeoima  12670  hmeocld  12672  fsumcncntop  12916
 Copyright terms: Public domain W3C validator