Theorem cdleme31id

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 18-Apr-2013)

	Ref	Expression
Hypothesis	cdleme31fv2.f	|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
Assertion	cdleme31id	|- ( ( X e. B /\ P = Q ) -> ( F ` X ) = X )

Proof

Step	Hyp	Ref	Expression
1		cdleme31fv2.f	|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
2		simpl	|- ( ( P =/= Q /\ -. X .<_ W ) -> P =/= Q )
3	2	necon2bi	|- ( P = Q -> -. ( P =/= Q /\ -. X .<_ W ) )
4	1	cdleme31fv2	|- ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) -> ( F ` X ) = X )
5	3 4	sylan2	|- ( ( X e. B /\ P = Q ) -> ( F ` X ) = X )