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

Metamath Proof Explorer

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 \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), O, x))$
	Assertion	cdleme31id	$⊢ (X \in B \land P = Q) \to F (X) = X$

Step	Hyp	Ref	Expression
1		cdleme31fv2.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), O, x))$
2		simpl	$⊢ (P \neq Q \land \neg X \underset{˙}{\leq} W) \to P \neq Q$
3	2	necon2bi	$⊢ P = Q \to \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)$
4	1	cdleme31fv2	$⊢ (X \in B \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = X$
5	3 4	sylan2	$⊢ (X \in B \land P = Q) \to F (X) = X$