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

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

Proof of Theorem syl5eqel
StepHypRef Expression
1 syl5eqel.1 . . 3 A = B
21a1i 9 . 2 (φA = B)
3 syl5eqel.2 . 2 (φB 𝐶)
42, 3eqeltrd 2111 1 (φA 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = 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:  syl5eqelr  2122  csbexga  3876  otexg  3958  tpexg  4145  dmresexg  4577  f1oabexg  5081  funfvex  5135  riotaexg  5415  riotaprop  5434  fnovex  5481  fovrn  5585  fnovrn  5590  cofunexg  5680  cofunex2g  5681  abrexex2g  5689  xpexgALT  5702  mpt2fvex  5771  tfrex  5895  frec0g  5922  ecexg  6046  qsexg  6098  negcl  6968  frecuzrdgrrn  8835  bj-snexg  9297
  Copyright terms: Public domain W3C validator