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 2732 | . 2 | |
2 | elex 2732 | . . 3 | |
3 | 2 | adantr 274 | . 2 |
4 | eleq1 2227 | . . . 4 | |
5 | eleq1 2227 | . . . . 5 | |
6 | 5 | notbid 657 | . . . 4 |
7 | 4, 6 | anbi12d 465 | . . 3 |
8 | df-dif 3113 | . . 3 | |
9 | 7, 8 | elab2g 2868 | . 2 |
10 | 1, 3, 9 | pm5.21nii 694 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wa 103 wb 104 wceq 1342 wcel 2135 cvv 2721 cdif 3108 |
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 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-dif 3113 |
This theorem is referenced by: eldifd 3121 eldifad 3122 eldifbd 3123 difeqri 3237 eldifi 3239 eldifn 3240 difdif 3242 ddifstab 3249 ssconb 3250 sscon 3251 ssdif 3252 raldifb 3257 dfss4st 3350 ssddif 3351 unssdif 3352 inssdif 3353 difin 3354 unssin 3356 inssun 3357 invdif 3359 indif 3360 difundi 3369 difindiss 3371 indifdir 3373 undif3ss 3378 difin2 3379 symdifxor 3383 dfnul2 3406 reldisj 3455 disj3 3456 undif4 3466 ssdif0im 3468 inssdif0im 3471 ssundifim 3487 eldifpr 3597 eldiftp 3616 eldifsn 3697 difprsnss 3705 iundif2ss 3925 iindif2m 3927 brdif 4029 unidif0 4140 eldifpw 4449 elirr 4512 en2lp 4525 difopab 4731 intirr 4984 cnvdif 5004 imadiflem 5261 imadif 5262 elfi2 6928 xrlenlt 7954 nzadd 9234 irradd 9575 irrmul 9576 fzdifsuc 10006 fisumss 11319 prodssdc 11516 fprodssdc 11517 inffinp1 12305 bj-charfunr 13533 |
Copyright terms: Public domain | W3C validator |