| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. |
| Ref | Expression |
|---|---|
| elin |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elisset 1855 |
. 2
| |
| 2 | elisset 1855 |
. . 3
| |
| 3 | 2 | adantl 388 |
. 2
|
| 4 | eleq1 1571 |
. . . 4
| |
| 5 | eleq1 1571 |
. . . 4
| |
| 6 | 4, 5 | anbi12d 630 |
. . 3
|
| 7 | df-in 2095 |
. . 3
| |
| 8 | 6, 7 | elab2g 1938 |
. 2
|
| 9 | 1, 3, 8 | pm5.21nii 682 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: incom 2252 ineqri 2253 ineq1 2254 hbin 2264 rabbirdv 2265 inass 2267 inss1 2274 ssrin 2278 dfss4 2286 dfin2 2288 difin 2289 indi 2295 undi 2296 unineq 2299 inab 2312 inrab2 2316 inelcm 2368 difin0ss 2377 inssdif0 2378 disjsn 2486 uniin 2568 intun 2610 intpr 2611 iunin2 2658 trin 2741 inex1 2767 frirr 2979 wefrc 2998 ordtri3or 3034 ordpwsuc 3121 brinxp2 3290 inopab 3334 inxp 3335 dmin 3382 opelres 3432 dfima2 3468 intasym 3501 asymref 3502 intirr 3504 cnvin 3512 dminss 3518 imainss 3519 ssrnres 3537 dfco3OLD 3569 dfco2a 3570 dfco4OLD 3571 funin 3641 2elresin 3673 nfvres 3824 funfvima 3928 isomin 3975 isoini 3976 tfrlem5 3991 tz7.48-2 4033 mapval2 4422 pw2en 4533 sbthcl 4546 ssenen 4593 inf3lem2 4700 zfregs 4733 cp 4808 bnd2 4810 aceq5lem1 4821 aceq5lem5 4825 aceq5 4826 kmlem3 4853 kmlem14 4864 kmlem15 4865 ltpiord 5104 ltxr 5584 clm4i 7203 infpss 7699 isbasis2g 7736 tgval2 7741 tgcl 7748 tgss3 7762 basgen 7764 opnin 7989 lmss 8073 isphg 8595 ishl 8710 axgroth4 8899 grothprim 8902 axhcompl 8987 hhcmpl 9189 ocin 9289 ocnel 9290 chocunii 9292 projlemHIL 9338 omlsilem 9364 pjoc1i 9384 shmodsi 9482 spansnm0i 9715 nonbooli 9716 5oalem1 9719 5oalem2 9720 5oalem4 9722 5oalem5 9723 5oalem7 9725 3oalem2 9728 3oalem3 9729 pjssmii 9746 mayete3i 9793 nmcopex 10076 nmcoplb 10077 lncnopbd 10083 nmcfnex 10105 nmcfnlb 10106 riesz4 10114 riesz1 10115 riesz2 10116 cnlnadjlem3 10119 cnlnadjlem4 10120 cnlnadjlem5 10121 cnlnadjlem9 10125 cnlnadjeu 10128 rnbra 10157 pjimai 10221 dfpjop 10228 pjclem4a 10244 pjclem4 10245 pj3lem1 10252 pj3si 10253 jpi 10315 sumdmdii 10460 sumdmdlem 10463 sumdmdlem2 10464 cdjreui 10477 cdj3lem1 10479 ntunte 10561 uninqs 10563 uninqsOLD 10564 domintref 10600 int2rel 10601 inposet 10619 filintf 10707 sfvlim 10729 fintopcomp 10747 topunfincomp 10748 usinuniop 10753 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 994 ax-gen 995 ax-8 996 ax-10 998 ax-12 1000 ax-17 1003 ax-4 1005 ax-5o 1007 ax-6o 1010 ax-9o 1155 ax-10o 1173 ax-16 1243 ax-11o 1251 ax-ext 1494 |
| This theorem depends on definitions: df-bi 145 df-an 223 df-ex 1013 df-sb 1205 df-clab 1500 df-cleq 1505 df-clel 1508 df-v 1850 df-in 2095 |