![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eldif | GIF version |
Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
eldif | ⊢ (A ∈ (B ∖ 𝐶) ↔ (A ∈ B ∧ ¬ A ∈ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2560 | . 2 ⊢ (A ∈ (B ∖ 𝐶) → A ∈ V) | |
2 | elex 2560 | . . 3 ⊢ (A ∈ B → A ∈ V) | |
3 | 2 | adantr 261 | . 2 ⊢ ((A ∈ B ∧ ¬ A ∈ 𝐶) → A ∈ V) |
4 | eleq1 2097 | . . . 4 ⊢ (x = A → (x ∈ B ↔ A ∈ B)) | |
5 | eleq1 2097 | . . . . 5 ⊢ (x = A → (x ∈ 𝐶 ↔ A ∈ 𝐶)) | |
6 | 5 | notbid 591 | . . . 4 ⊢ (x = A → (¬ x ∈ 𝐶 ↔ ¬ A ∈ 𝐶)) |
7 | 4, 6 | anbi12d 442 | . . 3 ⊢ (x = A → ((x ∈ B ∧ ¬ x ∈ 𝐶) ↔ (A ∈ B ∧ ¬ A ∈ 𝐶))) |
8 | df-dif 2914 | . . 3 ⊢ (B ∖ 𝐶) = {x ∣ (x ∈ B ∧ ¬ x ∈ 𝐶)} | |
9 | 7, 8 | elab2g 2683 | . 2 ⊢ (A ∈ V → (A ∈ (B ∖ 𝐶) ↔ (A ∈ B ∧ ¬ A ∈ 𝐶))) |
10 | 1, 3, 9 | pm5.21nii 619 | 1 ⊢ (A ∈ (B ∖ 𝐶) ↔ (A ∈ B ∧ ¬ A ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 97 ↔ wb 98 = wceq 1242 ∈ wcel 1390 Vcvv 2551 ∖ cdif 2908 |
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-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-v 2553 df-dif 2914 |
This theorem is referenced by: eldifd 2922 eldifad 2923 eldifbd 2924 difeqri 3058 eldifi 3060 eldifn 3061 difdif 3063 ssconb 3070 sscon 3071 ssdif 3072 raldifb 3077 ssddif 3165 unssdif 3166 inssdif 3167 difin 3168 unssin 3170 inssun 3171 invdif 3173 indif 3174 difundi 3183 difindiss 3185 indifdir 3187 undif3ss 3192 difin2 3193 symdifxor 3197 dfnul2 3220 reldisj 3265 disj3 3266 undif4 3278 ssdif0im 3280 inssdif0im 3285 ssundifim 3300 eldifsn 3486 difprsnss 3493 iundif2ss 3713 iindif2m 3715 brdif 3803 unidif0 3911 eldifpw 4174 elirr 4224 en2lp 4232 difopab 4412 intirr 4654 cnvdif 4673 imadiflem 4921 imadif 4922 xrlenlt 6881 irradd 8355 irrmul 8356 fzdifsuc 8713 |
Copyright terms: Public domain | W3C validator |