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

Theorem syl5eqel 2140
 Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eqel.1
syl5eqel.2
Assertion
Ref Expression
syl5eqel

Proof of Theorem syl5eqel
StepHypRef Expression
1 syl5eqel.1 . . 3
21a1i 9 . 2
3 syl5eqel.2 . 2
42, 3eqeltrd 2130 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1259   wcel 1409 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052 This theorem is referenced by:  syl5eqelr  2141  csbexga  3913  otexg  3995  tpexg  4207  dmresexg  4662  f1oabexg  5166  funfvex  5220  riotaexg  5500  riotaprop  5519  fnovex  5566  ovexg  5567  fovrn  5671  fnovrn  5676  cofunexg  5766  cofunex2g  5767  abrexex2g  5775  xpexgALT  5788  mpt2fvex  5857  tfrex  5985  frec0g  6014  ecexg  6141  qsexg  6193  diffifi  6382  addvalex  6978  negcl  7274  intqfrac2  9269  intfracq  9270  frecuzrdgrrn  9358  ibcval5  9631  climmpt  10052  ialgcvg  10270  ialgcvga  10273  ialgfx  10274  bj-snexg  10419
 Copyright terms: Public domain W3C validator