rusgrnumwwlkslem

		Ref	Expression
	Assertion	rusgrnumwwlkslem	$⊢ Y \in \{w \in Z \| w (0) = P\} \to \{w \in X \| (φ \land ψ)\} = \{w \in X \| (φ \land Y (0) = P \land ψ)\}$

Step	Hyp	Ref	Expression
1		fveq1	$⊢ w = Y \to w (0) = Y (0)$
2	1	eqeq1d	$⊢ w = Y \to (w (0) = P \leftrightarrow Y (0) = P)$
3	2	elrab	$⊢ Y \in \{w \in Z \| w (0) = P\} \leftrightarrow (Y \in Z \land Y (0) = P)$
4		ibar	$⊢ Y (0) = P \to ((φ \land ψ) \leftrightarrow (Y (0) = P \land (φ \land ψ)))$
5		3anass	$⊢ (Y (0) = P \land φ \land ψ) \leftrightarrow (Y (0) = P \land (φ \land ψ))$
6		3ancoma	$⊢ (Y (0) = P \land φ \land ψ) \leftrightarrow (φ \land Y (0) = P \land ψ)$
7	5 6	bitr3i	$⊢ (Y (0) = P \land (φ \land ψ)) \leftrightarrow (φ \land Y (0) = P \land ψ)$
8	4 7	bitrdi	$⊢ Y (0) = P \to ((φ \land ψ) \leftrightarrow (φ \land Y (0) = P \land ψ))$
9	8	ad2antlr	$⊢ ((Y \in Z \land Y (0) = P) \land w \in X) \to ((φ \land ψ) \leftrightarrow (φ \land Y (0) = P \land ψ))$
10	9	rabbidva	$⊢ (Y \in Z \land Y (0) = P) \to \{w \in X \| (φ \land ψ)\} = \{w \in X \| (φ \land Y (0) = P \land ψ)\}$
11	3 10	sylbi	$⊢ Y \in \{w \in Z \| w (0) = P\} \to \{w \in X \| (φ \land ψ)\} = \{w \in X \| (φ \land Y (0) = P \land ψ)\}$

Metamath Proof Explorer