![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eldifi | GIF version |
Description: Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
eldifi | ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldif 3150 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) | |
2 | 1 | simplbi 274 | 1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2158 ∖ cdif 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-v 2751 df-dif 3143 |
This theorem is referenced by: difss 3273 ssddif 3381 noel 3438 phpm 6879 fidifsnen 6884 elfi2 6985 fiuni 6991 fifo 6993 fzdifsuc 10095 modfzo0difsn 10409 fsum3cvg 11400 summodclem2a 11403 fisumss 11414 fsumlessfi 11482 binomlem 11505 fproddccvg 11594 prodmodclem2a 11598 fprodssdc 11612 fprodeq0g 11660 fprodmodd 11663 oddprmge3 12149 oddprm 12273 nnoddn2prm 12274 nnoddn2prmb 12276 grpinvnzcl 12969 ringelnzr 13407 2irrexpqap 14692 lgslem1 14697 lgslem4 14700 lgsvalmod 14716 m1lgs 14748 |
Copyright terms: Public domain | W3C validator |