![]() |
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 2611 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2611 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 2 | adantr 270 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
4 | eleq1 2142 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | eleq1 2142 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
6 | 5 | notbid 625 | . . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶)) |
7 | 4, 6 | anbi12d 457 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))) |
8 | df-dif 2976 | . . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)} | |
9 | 7, 8 | elab2g 2741 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))) |
10 | 1, 3, 9 | pm5.21nii 653 | 1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 102 ↔ wb 103 = wceq 1285 ∈ wcel 1434 Vcvv 2602 ∖ cdif 2971 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-v 2604 df-dif 2976 |
This theorem is referenced by: eldifd 2984 eldifad 2985 eldifbd 2986 difeqri 3093 eldifi 3095 eldifn 3096 difdif 3098 ddifstab 3105 ssconb 3106 sscon 3107 ssdif 3108 raldifb 3113 ssddif 3199 unssdif 3200 inssdif 3201 difin 3202 unssin 3204 inssun 3205 invdif 3207 indif 3208 difundi 3217 difindiss 3219 indifdir 3221 undif3ss 3226 difin2 3227 symdifxor 3231 dfnul2 3254 reldisj 3296 disj3 3297 undif4 3307 ssdif0im 3309 inssdif0im 3312 ssundifim 3327 eldifsn 3519 difprsnss 3526 iundif2ss 3745 iindif2m 3747 brdif 3835 unidif0 3943 eldifpw 4228 elirr 4286 en2lp 4299 difopab 4491 intirr 4735 cnvdif 4754 imadiflem 5003 imadif 5004 xrlenlt 7233 nzadd 8473 irradd 8801 irrmul 8802 fzdifsuc 9163 |
Copyright terms: Public domain | W3C validator |