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 2697 | . 2 | |
2 | elex 2697 | . . 3 | |
3 | 2 | adantr 274 | . 2 |
4 | eleq1 2202 | . . . 4 | |
5 | eleq1 2202 | . . . . 5 | |
6 | 5 | notbid 656 | . . . 4 |
7 | 4, 6 | anbi12d 464 | . . 3 |
8 | df-dif 3073 | . . 3 | |
9 | 7, 8 | elab2g 2831 | . 2 |
10 | 1, 3, 9 | pm5.21nii 693 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wa 103 wb 104 wceq 1331 wcel 1480 cvv 2686 cdif 3068 |
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 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-dif 3073 |
This theorem is referenced by: eldifd 3081 eldifad 3082 eldifbd 3083 difeqri 3196 eldifi 3198 eldifn 3199 difdif 3201 ddifstab 3208 ssconb 3209 sscon 3210 ssdif 3211 raldifb 3216 dfss4st 3309 ssddif 3310 unssdif 3311 inssdif 3312 difin 3313 unssin 3315 inssun 3316 invdif 3318 indif 3319 difundi 3328 difindiss 3330 indifdir 3332 undif3ss 3337 difin2 3338 symdifxor 3342 dfnul2 3365 reldisj 3414 disj3 3415 undif4 3425 ssdif0im 3427 inssdif0im 3430 ssundifim 3446 eldifsn 3650 difprsnss 3658 iundif2ss 3878 iindif2m 3880 brdif 3981 unidif0 4091 eldifpw 4398 elirr 4456 en2lp 4469 difopab 4672 intirr 4925 cnvdif 4945 imadiflem 5202 imadif 5203 elfi2 6860 xrlenlt 7829 nzadd 9106 irradd 9438 irrmul 9439 fzdifsuc 9861 fisumss 11161 inffinp1 11942 |
Copyright terms: Public domain | W3C validator |