![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elfpw | Structured version Visualization version GIF version |
Description: Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Ref | Expression |
---|---|
elfpw | ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3939 | . 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin)) | |
2 | elpwg 4310 | . . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 2 | pm5.32ri 673 | . 2 ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) |
4 | 1, 3 | bitri 264 | 1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∈ wcel 2139 ∩ cin 3714 ⊆ wss 3715 𝒫 cpw 4302 Fincfn 8123 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-in 3722 df-ss 3729 df-pw 4304 |
This theorem is referenced by: bitsinv2 15387 bitsf1ocnv 15388 2ebits 15391 bitsinvp1 15393 sadcaddlem 15401 sadadd2lem 15403 sadadd3 15405 sadaddlem 15410 sadasslem 15414 sadeq 15416 firest 16315 acsfiindd 17398 restfpw 21205 cmpcov2 21415 cmpcovf 21416 cncmp 21417 tgcmp 21426 cmpcld 21427 cmpfi 21433 locfincmp 21551 comppfsc 21557 alexsublem 22069 alexsubALTlem2 22073 alexsubALTlem4 22075 alexsubALT 22076 ptcmplem2 22078 ptcmplem3 22079 ptcmplem5 22081 tsmsfbas 22152 tsmslem1 22153 tsmsgsum 22163 tsmssubm 22167 tsmsres 22168 tsmsf1o 22169 tsmsmhm 22170 tsmsadd 22171 tsmsxplem1 22177 tsmsxplem2 22178 tsmsxp 22179 xrge0gsumle 22857 xrge0tsms 22858 xrge0tsmsd 30115 indf1ofs 30418 mvrsfpw 31731 elmpst 31761 istotbnd3 33901 sstotbnd2 33904 sstotbnd 33905 sstotbnd3 33906 equivtotbnd 33908 totbndbnd 33919 prdstotbnd 33924 isnacs3 37793 pwfi2f1o 38186 hbtlem6 38219 |
Copyright terms: Public domain | W3C validator |