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 | ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2566 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2566 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 2 | adantr 261 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
4 | eleq1 2100 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | eleq1 2100 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
6 | 5 | notbid 592 | . . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶)) |
7 | 4, 6 | anbi12d 442 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))) |
8 | df-dif 2920 | . . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)} | |
9 | 7, 8 | elab2g 2689 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))) |
10 | 1, 3, 9 | pm5.21nii 620 | 1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 97 ↔ wb 98 = wceq 1243 ∈ wcel 1393 Vcvv 2557 ∖ cdif 2914 |
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 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-v 2559 df-dif 2920 |
This theorem is referenced by: eldifd 2928 eldifad 2929 eldifbd 2930 difeqri 3064 eldifi 3066 eldifn 3067 difdif 3069 ssconb 3076 sscon 3077 ssdif 3078 raldifb 3083 ssddif 3171 unssdif 3172 inssdif 3173 difin 3174 unssin 3176 inssun 3177 invdif 3179 indif 3180 difundi 3189 difindiss 3191 indifdir 3193 undif3ss 3198 difin2 3199 symdifxor 3203 dfnul2 3226 reldisj 3271 disj3 3272 undif4 3284 ssdif0im 3286 inssdif0im 3291 ssundifim 3306 eldifsn 3495 difprsnss 3502 iundif2ss 3722 iindif2m 3724 brdif 3812 unidif0 3920 eldifpw 4208 elirr 4266 en2lp 4278 difopab 4469 intirr 4711 cnvdif 4730 imadiflem 4978 imadif 4979 xrlenlt 7084 irradd 8580 irrmul 8581 fzdifsuc 8943 |
Copyright terms: Public domain | W3C validator |