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

Theorem elfpw 8309
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 3829 . 2 (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵𝐴 ∈ Fin))
2 elpwg 4199 . . 3 (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
32pm5.32ri 671 . 2 ((𝐴 ∈ 𝒫 𝐵𝐴 ∈ Fin) ↔ (𝐴𝐵𝐴 ∈ Fin))
41, 3bitri 264 1 (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴𝐵𝐴 ∈ Fin))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wcel 2030  cin 3606  wss 3607  𝒫 cpw 4191  Fincfn 7997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193
This theorem is referenced by:  bitsinv2  15212  bitsf1ocnv  15213  2ebits  15216  bitsinvp1  15218  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  sadaddlem  15235  sadasslem  15239  sadeq  15241  firest  16140  acsfiindd  17224  restfpw  21031  cmpcov2  21241  cmpcovf  21242  cncmp  21243  tgcmp  21252  cmpcld  21253  cmpfi  21259  locfincmp  21377  comppfsc  21383  alexsublem  21895  alexsubALTlem2  21899  alexsubALTlem4  21901  alexsubALT  21902  ptcmplem2  21904  ptcmplem3  21905  ptcmplem5  21907  tsmsfbas  21978  tsmslem1  21979  tsmsgsum  21989  tsmssubm  21993  tsmsres  21994  tsmsf1o  21995  tsmsmhm  21996  tsmsadd  21997  tsmsxplem1  22003  tsmsxplem2  22004  tsmsxp  22005  xrge0gsumle  22683  xrge0tsms  22684  xrge0tsmsd  29913  indf1ofs  30216  mvrsfpw  31529  elmpst  31559  istotbnd3  33700  sstotbnd2  33703  sstotbnd  33704  sstotbnd3  33705  equivtotbnd  33707  totbndbnd  33718  prdstotbnd  33723  isnacs3  37590  pwfi2f1o  37983  hbtlem6  38016
  Copyright terms: Public domain W3C validator