![]() |
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 2748 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2748 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | adantr 276 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eleq1 2240 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eleq1 2240 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | notbid 667 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | anbi12d 473 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | df-dif 3131 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | elab2g 2884 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 1, 3, 9 | pm5.21nii 704 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-dif 3131 |
This theorem is referenced by: eldifd 3139 eldifad 3140 eldifbd 3141 difeqri 3255 eldifi 3257 eldifn 3258 difdif 3260 ddifstab 3267 ssconb 3268 sscon 3269 ssdif 3270 raldifb 3275 dfss4st 3368 ssddif 3369 unssdif 3370 inssdif 3371 difin 3372 unssin 3374 inssun 3375 invdif 3377 indif 3378 difundi 3387 difindiss 3389 indifdir 3391 undif3ss 3396 difin2 3397 symdifxor 3401 dfnul2 3424 reldisj 3474 disj3 3475 undif4 3485 ssdif0im 3487 inssdif0im 3490 ssundifim 3506 eldifpr 3618 eldiftp 3637 eldifsn 3718 difprsnss 3729 iundif2ss 3949 iindif2m 3951 brdif 4053 unidif0 4164 eldifpw 4473 elirr 4536 en2lp 4549 difopab 4755 intirr 5010 cnvdif 5030 imadiflem 5290 imadif 5291 elfi2 6964 xrlenlt 7999 nzadd 9281 irradd 9622 irrmul 9623 fzdifsuc 10054 fisumss 11371 prodssdc 11568 fprodssdc 11569 inffinp1 12400 bj-charfunr 14184 |
Copyright terms: Public domain | W3C validator |