![]() |
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 2763 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2763 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | adantl 277 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eleq1 2252 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eleq1 2252 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | anbi12d 473 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | df-in 3150 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | elab2g 2899 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 1, 3, 8 | pm5.21nii 705 |
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-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-in 3150 |
This theorem is referenced by: elini 3334 elind 3335 elinel1 3336 elinel2 3337 elin2 3338 elin3 3341 incom 3342 ineqri 3343 ineq1 3344 inass 3360 inss1 3370 ssin 3372 ssrin 3375 dfss4st 3383 inssdif 3386 difin 3387 unssin 3389 inssun 3390 invdif 3392 indif 3393 indi 3397 undi 3398 difundi 3402 difindiss 3404 indifdir 3406 difin2 3412 inrab2 3423 inelcm 3498 inssdif0im 3505 uniin 3844 intun 3890 intpr 3891 elrint 3899 iunin2 3965 iinin2m 3970 elriin 3972 disjnim 4009 disjiun 4013 brin 4070 trin 4126 inex1 4152 inuni 4170 bnd2 4188 ordpwsucss 4581 ordpwsucexmid 4584 peano5 4612 inopab 4774 inxp 4776 dmin 4850 opelres 4927 intasym 5028 asymref 5029 dminss 5058 imainss 5059 inimasn 5061 ssrnres 5086 cnvresima 5133 dfco2a 5144 funinsn 5281 imainlem 5313 imain 5314 2elresin 5343 nfvres 5564 respreima 5661 isoini 5836 offval 6109 tfrlem5 6334 mapval2 6699 ixpin 6744 ssenen 6874 infidc 6959 fnfi 6961 peano5nnnn 7916 peano5nni 8947 ixxdisj 9928 icodisj 10017 fzdisj 10077 uzdisj 10118 nn0disj 10163 fzouzdisj 10205 isumss 11426 fsumsplit 11442 sumsplitdc 11467 fsum2dlemstep 11469 fprod2dlemstep 11657 4sqlem12 12429 nninfdclemcl 12494 nninfdclemp1 12496 insubm 12930 isrhm 13501 subsubrng2 13555 subsubrg2 13586 2idlelb 13813 isbasis2g 13982 tgval2 13988 tgcl 14001 epttop 14027 ssntr 14059 ntreq0 14069 cnptopresti 14175 cnptoprest 14176 cnptoprest2 14177 lmss 14183 txcnp 14208 txcnmpt 14210 bldisj 14338 blininf 14361 blres 14371 metrest 14443 pilem1 14637 bj-charfundcALT 14999 bj-charfunr 15000 bdinex1 15089 bj-indind 15122 |
Copyright terms: Public domain | W3C validator |