![]() |
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 2652 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2652 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | adantr 272 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eleq1 2162 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eleq1 2162 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | notbid 633 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | anbi12d 460 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | df-dif 3023 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | elab2g 2784 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 1, 3, 9 | pm5.21nii 661 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-dif 3023 |
This theorem is referenced by: eldifd 3031 eldifad 3032 eldifbd 3033 difeqri 3143 eldifi 3145 eldifn 3146 difdif 3148 ddifstab 3155 ssconb 3156 sscon 3157 ssdif 3158 raldifb 3163 dfss4st 3256 ssddif 3257 unssdif 3258 inssdif 3259 difin 3260 unssin 3262 inssun 3263 invdif 3265 indif 3266 difundi 3275 difindiss 3277 indifdir 3279 undif3ss 3284 difin2 3285 symdifxor 3289 dfnul2 3312 reldisj 3361 disj3 3362 undif4 3372 ssdif0im 3374 inssdif0im 3377 ssundifim 3393 eldifsn 3597 difprsnss 3605 iundif2ss 3825 iindif2m 3827 brdif 3923 unidif0 4031 eldifpw 4336 elirr 4394 en2lp 4407 difopab 4610 intirr 4861 cnvdif 4881 imadiflem 5138 imadif 5139 xrlenlt 7701 nzadd 8958 irradd 9288 irrmul 9289 fzdifsuc 9702 fisumss 11000 inffinp1 11734 |
Copyright terms: Public domain | W3C validator |