Metamath Proof Explorer


Theorem cdleme31fv1s

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

Ref Expression
Hypotheses cdleme31.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme31.f F = x B if P Q ¬ x ˙ W O x
Assertion cdleme31fv1s X B P Q ¬ X ˙ W F X = X / x O

Proof

Step Hyp Ref Expression
1 cdleme31.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
2 cdleme31.f F = x B if P Q ¬ x ˙ W O x
3 eqid ι z B | s A ¬ s ˙ W s ˙ X ˙ W = X z = N ˙ X ˙ W = ι z B | s A ¬ s ˙ W s ˙ X ˙ W = X z = N ˙ X ˙ W
4 1 2 3 cdleme31fv1 X B P Q ¬ X ˙ W F X = ι z B | s A ¬ s ˙ W s ˙ X ˙ W = X z = N ˙ X ˙ W
5 1 3 cdleme31so X B X / x O = ι z B | s A ¬ s ˙ W s ˙ X ˙ W = X z = N ˙ X ˙ W
6 5 adantr X B P Q ¬ X ˙ W X / x O = ι z B | s A ¬ s ˙ W s ˙ X ˙ W = X z = N ˙ X ˙ W
7 4 6 eqtr4d X B P Q ¬ X ˙ W F X = X / x O