This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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