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 ) )