Metamath Proof Explorer

Theorem elfpw

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
Assertion elfpw 
|- ( A e. ( ~P B i^i Fin ) <-> ( A C_ B /\ A e. Fin ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( A e. ( ~P B i^i Fin ) <-> ( A e. ~P B /\ A e. Fin ) )
2 elpwg 
 |-  ( A e. Fin -> ( A e. ~P B <-> A C_ B ) )
3 2 pm5.32ri 
 |-  ( ( A e. ~P B /\ A e. Fin ) <-> ( A C_ B /\ A e. Fin ) )
4 1 3 bitri 
 |-  ( A e. ( ~P B i^i Fin ) <-> ( A C_ B /\ A e. Fin ) )