Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elin | Unicode version |
Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
elin |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2697 | . 2 | |
2 | elex 2697 | . . 3 | |
3 | 2 | adantl 275 | . 2 |
4 | eleq1 2202 | . . . 4 | |
5 | eleq1 2202 | . . . 4 | |
6 | 4, 5 | anbi12d 464 | . . 3 |
7 | df-in 3077 | . . 3 | |
8 | 6, 7 | elab2g 2831 | . 2 |
9 | 1, 3, 8 | pm5.21nii 693 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wceq 1331 wcel 1480 cvv 2686 cin 3070 |
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-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-in 3077 |
This theorem is referenced by: elini 3260 elind 3261 elinel1 3262 elinel2 3263 elin2 3264 elin3 3267 incom 3268 ineqri 3269 ineq1 3270 inass 3286 inss1 3296 ssin 3298 ssrin 3301 dfss4st 3309 inssdif 3312 difin 3313 unssin 3315 inssun 3316 invdif 3318 indif 3319 indi 3323 undi 3324 difundi 3328 difindiss 3330 indifdir 3332 difin2 3338 inrab2 3349 inelcm 3423 inssdif0im 3430 uniin 3756 intun 3802 intpr 3803 elrint 3811 iunin2 3876 iinin2m 3881 elriin 3883 disjnim 3920 disjiun 3924 brin 3980 trin 4036 inex1 4062 inuni 4080 bnd2 4097 ordpwsucss 4482 ordpwsucexmid 4485 peano5 4512 inopab 4671 inxp 4673 dmin 4747 opelres 4824 intasym 4923 asymref 4924 dminss 4953 imainss 4954 inimasn 4956 ssrnres 4981 cnvresima 5028 dfco2a 5039 funinsn 5172 imainlem 5204 imain 5205 2elresin 5234 nfvres 5454 respreima 5548 isoini 5719 offval 5989 tfrlem5 6211 mapval2 6572 ixpin 6617 ssenen 6745 fnfi 6825 peano5nnnn 7700 peano5nni 8723 ixxdisj 9686 icodisj 9775 fzdisj 9832 uzdisj 9873 nn0disj 9915 fzouzdisj 9957 isumss 11160 fsumsplit 11176 sumsplitdc 11201 fsum2dlemstep 11203 isbasis2g 12212 tgval2 12220 tgcl 12233 epttop 12259 ssntr 12291 ntreq0 12301 cnptopresti 12407 cnptoprest 12408 cnptoprest2 12409 lmss 12415 txcnp 12440 txcnmpt 12442 bldisj 12570 blininf 12593 blres 12603 metrest 12675 pilem1 12860 bdinex1 13097 bj-indind 13130 |
Copyright terms: Public domain | W3C validator |