MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfpw Structured version   Visualization version   GIF version

Theorem elfpw 9305
Description: Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Assertion
Ref Expression
elfpw (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴𝐵𝐴 ∈ Fin))

Proof of Theorem elfpw
StepHypRef Expression
1 elin 3931 . 2 (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵𝐴 ∈ Fin))
2 elpwg 4568 . . 3 (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
32pm5.32ri 577 . 2 ((𝐴 ∈ 𝒫 𝐵𝐴 ∈ Fin) ↔ (𝐴𝐵𝐴 ∈ Fin))
41, 3bitri 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