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 2741 | . 2 | |
2 | elex 2741 | . . 3 | |
3 | 2 | adantl 275 | . 2 |
4 | eleq1 2233 | . . . 4 | |
5 | eleq1 2233 | . . . 4 | |
6 | 4, 5 | anbi12d 470 | . . 3 |
7 | df-in 3127 | . . 3 | |
8 | 6, 7 | elab2g 2877 | . 2 |
9 | 1, 3, 8 | pm5.21nii 699 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wceq 1348 wcel 2141 cvv 2730 cin 3120 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-v 2732 df-in 3127 |
This theorem is referenced by: elini 3311 elind 3312 elinel1 3313 elinel2 3314 elin2 3315 elin3 3318 incom 3319 ineqri 3320 ineq1 3321 inass 3337 inss1 3347 ssin 3349 ssrin 3352 dfss4st 3360 inssdif 3363 difin 3364 unssin 3366 inssun 3367 invdif 3369 indif 3370 indi 3374 undi 3375 difundi 3379 difindiss 3381 indifdir 3383 difin2 3389 inrab2 3400 inelcm 3474 inssdif0im 3481 uniin 3814 intun 3860 intpr 3861 elrint 3869 iunin2 3934 iinin2m 3939 elriin 3941 disjnim 3978 disjiun 3982 brin 4039 trin 4095 inex1 4121 inuni 4139 bnd2 4157 ordpwsucss 4549 ordpwsucexmid 4552 peano5 4580 inopab 4741 inxp 4743 dmin 4817 opelres 4894 intasym 4993 asymref 4994 dminss 5023 imainss 5024 inimasn 5026 ssrnres 5051 cnvresima 5098 dfco2a 5109 funinsn 5245 imainlem 5277 imain 5278 2elresin 5307 nfvres 5527 respreima 5621 isoini 5794 offval 6065 tfrlem5 6290 mapval2 6652 ixpin 6697 ssenen 6825 fnfi 6910 peano5nnnn 7841 peano5nni 8868 ixxdisj 9847 icodisj 9936 fzdisj 9995 uzdisj 10036 nn0disj 10081 fzouzdisj 10123 isumss 11341 fsumsplit 11357 sumsplitdc 11382 fsum2dlemstep 11384 fprod2dlemstep 11572 nninfdclemcl 12390 nninfdclemp1 12392 insubm 12690 isbasis2g 12796 tgval2 12804 tgcl 12817 epttop 12843 ssntr 12875 ntreq0 12885 cnptopresti 12991 cnptoprest 12992 cnptoprest2 12993 lmss 12999 txcnp 13024 txcnmpt 13026 bldisj 13154 blininf 13177 blres 13187 metrest 13259 pilem1 13453 bj-charfundcALT 13804 bj-charfunr 13805 bdinex1 13894 bj-indind 13927 |
Copyright terms: Public domain | W3C validator |