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 2741 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2741 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 2 | adantr 274 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
4 | eleq1 2233 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | eleq1 2233 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
6 | 5 | notbid 662 | . . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶)) |
7 | 4, 6 | anbi12d 470 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))) |
8 | df-dif 3123 | . . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)} | |
9 | 7, 8 | elab2g 2877 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))) |
10 | 1, 3, 9 | pm5.21nii 699 | 1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 103 ↔ wb 104 = wceq 1348 ∈ wcel 2141 Vcvv 2730 ∖ cdif 3118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-v 2732 df-dif 3123 |
This theorem is referenced by: eldifd 3131 eldifad 3132 eldifbd 3133 difeqri 3247 eldifi 3249 eldifn 3250 difdif 3252 ddifstab 3259 ssconb 3260 sscon 3261 ssdif 3262 raldifb 3267 dfss4st 3360 ssddif 3361 unssdif 3362 inssdif 3363 difin 3364 unssin 3366 inssun 3367 invdif 3369 indif 3370 difundi 3379 difindiss 3381 indifdir 3383 undif3ss 3388 difin2 3389 symdifxor 3393 dfnul2 3416 reldisj 3466 disj3 3467 undif4 3477 ssdif0im 3479 inssdif0im 3482 ssundifim 3498 eldifpr 3610 eldiftp 3629 eldifsn 3710 difprsnss 3718 iundif2ss 3938 iindif2m 3940 brdif 4042 unidif0 4153 eldifpw 4462 elirr 4525 en2lp 4538 difopab 4744 intirr 4997 cnvdif 5017 imadiflem 5277 imadif 5278 elfi2 6949 xrlenlt 7984 nzadd 9264 irradd 9605 irrmul 9606 fzdifsuc 10037 fisumss 11355 prodssdc 11552 fprodssdc 11553 inffinp1 12384 bj-charfunr 13845 |
Copyright terms: Public domain | W3C validator |