| 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 3967 | . 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin)) | |
| 2 | elpwg 4603 | . . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
| 3 | 2 | pm5.32ri 575 | . 2 ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) |
| 4 | 1, 3 | bitri 275 | 1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∈ wcel 2108 ∩ cin 3950 ⊆ wss 3951 𝒫 cpw 4600 Fincfn 8985 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: bitsinv2 16480 bitsf1ocnv 16481 2ebits 16484 bitsinvp1 16486 sadcaddlem 16494 sadadd2lem 16496 sadadd3 16498 sadaddlem 16503 sadasslem 16507 sadeq 16509 firest 17477 acsfiindd 18598 restfpw 23187 cmpcov2 23398 cmpcovf 23399 cncmp 23400 tgcmp 23409 cmpcld 23410 cmpfi 23416 locfincmp 23534 comppfsc 23540 alexsublem 24052 alexsubALTlem2 24056 alexsubALTlem4 24058 alexsubALT 24059 ptcmplem2 24061 ptcmplem3 24062 ptcmplem5 24064 tsmsfbas 24136 tsmslem1 24137 tsmsgsum 24147 tsmssubm 24151 tsmsres 24152 tsmsf1o 24153 tsmsmhm 24154 tsmsadd 24155 tsmsxplem1 24161 tsmsxplem2 24162 tsmsxp 24163 xrge0gsumle 24855 xrge0tsms 24856 indf1ofs 32851 xrge0tsmsd 33065 mvrsfpw 35511 elmpst 35541 istotbnd3 37778 sstotbnd2 37781 sstotbnd 37782 sstotbnd3 37783 equivtotbnd 37785 totbndbnd 37796 prdstotbnd 37801 isnacs3 42721 pwfi2f1o 43108 hbtlem6 43141 |
| Copyright terms: Public domain | W3C validator |