Metamath Proof Explorer


Theorem isf34lem1

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypothesis compss.a
|- F = ( x e. ~P A |-> ( A \ x ) )
Assertion isf34lem1
|- ( ( A e. V /\ X C_ A ) -> ( F ` X ) = ( A \ X ) )

Proof

Step Hyp Ref Expression
1 compss.a
 |-  F = ( x e. ~P A |-> ( A \ x ) )
2 difeq2
 |-  ( x = a -> ( A \ x ) = ( A \ a ) )
3 2 cbvmptv
 |-  ( x e. ~P A |-> ( A \ x ) ) = ( a e. ~P A |-> ( A \ a ) )
4 1 3 eqtri
 |-  F = ( a e. ~P A |-> ( A \ a ) )
5 difeq2
 |-  ( a = X -> ( A \ a ) = ( A \ X ) )
6 elpw2g
 |-  ( A e. V -> ( X e. ~P A <-> X C_ A ) )
7 6 biimpar
 |-  ( ( A e. V /\ X C_ A ) -> X e. ~P A )
8 difexg
 |-  ( A e. V -> ( A \ X ) e. _V )
9 8 adantr
 |-  ( ( A e. V /\ X C_ A ) -> ( A \ X ) e. _V )
10 4 5 7 9 fvmptd3
 |-  ( ( A e. V /\ X C_ A ) -> ( F ` X ) = ( A \ X ) )