Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eldif | Unicode version |
Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
eldif |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2671 | . 2 | |
2 | elex 2671 | . . 3 | |
3 | 2 | adantr 274 | . 2 |
4 | eleq1 2180 | . . . 4 | |
5 | eleq1 2180 | . . . . 5 | |
6 | 5 | notbid 641 | . . . 4 |
7 | 4, 6 | anbi12d 464 | . . 3 |
8 | df-dif 3043 | . . 3 | |
9 | 7, 8 | elab2g 2804 | . 2 |
10 | 1, 3, 9 | pm5.21nii 678 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wa 103 wb 104 wceq 1316 wcel 1465 cvv 2660 cdif 3038 |
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 588 ax-in2 589 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 df-dif 3043 |
This theorem is referenced by: eldifd 3051 eldifad 3052 eldifbd 3053 difeqri 3166 eldifi 3168 eldifn 3169 difdif 3171 ddifstab 3178 ssconb 3179 sscon 3180 ssdif 3181 raldifb 3186 dfss4st 3279 ssddif 3280 unssdif 3281 inssdif 3282 difin 3283 unssin 3285 inssun 3286 invdif 3288 indif 3289 difundi 3298 difindiss 3300 indifdir 3302 undif3ss 3307 difin2 3308 symdifxor 3312 dfnul2 3335 reldisj 3384 disj3 3385 undif4 3395 ssdif0im 3397 inssdif0im 3400 ssundifim 3416 eldifsn 3620 difprsnss 3628 iundif2ss 3848 iindif2m 3850 brdif 3951 unidif0 4061 eldifpw 4368 elirr 4426 en2lp 4439 difopab 4642 intirr 4895 cnvdif 4915 imadiflem 5172 imadif 5173 elfi2 6828 xrlenlt 7797 nzadd 9074 irradd 9406 irrmul 9407 fzdifsuc 9829 fisumss 11129 inffinp1 11869 |
Copyright terms: Public domain | W3C validator |