![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5eqel | GIF version |
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
syl5eqel.1 | ⊢ A = B |
syl5eqel.2 | ⊢ (φ → B ∈ 𝐶) |
Ref | Expression |
---|---|
syl5eqel | ⊢ (φ → A ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5eqel.1 | . . 3 ⊢ A = B | |
2 | 1 | a1i 9 | . 2 ⊢ (φ → A = B) |
3 | syl5eqel.2 | . 2 ⊢ (φ → B ∈ 𝐶) | |
4 | 2, 3 | eqeltrd 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 7008 frecuzrdgrrn 8875 bj-snexg 9367 |
Copyright terms: Public domain | W3C validator |