Metamath Proof Explorer


Theorem cdleme31fv2

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

Ref Expression
Hypothesis cdleme31fv2.f F=xBifPQ¬x˙WOx
Assertion cdleme31fv2 XB¬PQ¬X˙WFX=X

Proof

Step Hyp Ref Expression
1 cdleme31fv2.f F=xBifPQ¬x˙WOx
2 breq1 x=Xx˙WX˙W
3 2 notbid x=X¬x˙W¬X˙W
4 3 anbi2d x=XPQ¬x˙WPQ¬X˙W
5 4 notbid x=X¬PQ¬x˙W¬PQ¬X˙W
6 5 biimparc ¬PQ¬X˙Wx=X¬PQ¬x˙W
7 6 adantll XB¬PQ¬X˙Wx=X¬PQ¬x˙W
8 7 iffalsed XB¬PQ¬X˙Wx=XifPQ¬x˙WOx=x
9 simpr XB¬PQ¬X˙Wx=Xx=X
10 8 9 eqtrd XB¬PQ¬X˙Wx=XifPQ¬x˙WOx=X
11 simpl XB¬PQ¬X˙WXB
12 1 10 11 11 fvmptd2 XB¬PQ¬X˙WFX=X