![]() |
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 3931 | . 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin)) | |
2 | elpwg 4568 | . . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 2 | pm5.32ri 577 | . 2 ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) |
4 | 1, 3 | bitri 275 | 1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∈ wcel 2107 ∩ cin 3914 ⊆ wss 3915 𝒫 cpw 4565 Fincfn 8890 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 df-pw 4567 |
This theorem is referenced by: bitsinv2 16330 bitsf1ocnv 16331 2ebits 16334 bitsinvp1 16336 sadcaddlem 16344 sadadd2lem 16346 sadadd3 16348 sadaddlem 16353 sadasslem 16357 sadeq 16359 firest 17321 acsfiindd 18449 restfpw 22546 cmpcov2 22757 cmpcovf 22758 cncmp 22759 tgcmp 22768 cmpcld 22769 cmpfi 22775 locfincmp 22893 comppfsc 22899 alexsublem 23411 alexsubALTlem2 23415 alexsubALTlem4 23417 alexsubALT 23418 ptcmplem2 23420 ptcmplem3 23421 ptcmplem5 23423 tsmsfbas 23495 tsmslem1 23496 tsmsgsum 23506 tsmssubm 23510 tsmsres 23511 tsmsf1o 23512 tsmsmhm 23513 tsmsadd 23514 tsmsxplem1 23520 tsmsxplem2 23521 tsmsxp 23522 xrge0gsumle 24212 xrge0tsms 24213 xrge0tsmsd 31941 indf1ofs 32665 mvrsfpw 34140 elmpst 34170 istotbnd3 36259 sstotbnd2 36262 sstotbnd 36263 sstotbnd3 36264 equivtotbnd 36266 totbndbnd 36277 prdstotbnd 36282 isnacs3 41062 pwfi2f1o 41452 hbtlem6 41485 |
Copyright terms: Public domain | W3C validator |