Metamath Proof Explorer

Theorem rusgrnumwwlkslem

Description: Lemma for rusgrnumwwlks . (Contributed by Alexander van der Vekens, 23-Aug-2018)

Ref Expression
Assertion rusgrnumwwlkslem ⊢ Y ∈ w ∈ Z | w ⁡ 0 = P → w ∈ X | φ ∧ ψ = w ∈ X | φ ∧ Y ⁡ 0 = P ∧ ψ

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ w = Y → w ⁡ 0 = Y ⁡ 0
2 1 eqeq1d ⊢ w = Y → w ⁡ 0 = P ↔ Y ⁡ 0 = P
3 2 elrab ⊢ Y ∈ w ∈ Z | w ⁡ 0 = P ↔ Y ∈ Z ∧ Y ⁡ 0 = P
4 ibar ⊢ Y ⁡ 0 = P → φ ∧ ψ ↔ Y ⁡ 0 = P ∧ φ ∧ ψ
5 3anass ⊢ Y ⁡ 0 = P ∧ φ ∧ ψ ↔ Y ⁡ 0 = P ∧ φ ∧ ψ
6 3ancoma ⊢ Y ⁡ 0 = P ∧ φ ∧ ψ ↔ φ ∧ Y ⁡ 0 = P ∧ ψ
7 5 6 bitr3i ⊢ Y ⁡ 0 = P ∧ φ ∧ ψ ↔ φ ∧ Y ⁡ 0 = P ∧ ψ
8 4 7 bitrdi ⊢ Y ⁡ 0 = P → φ ∧ ψ ↔ φ ∧ Y ⁡ 0 = P ∧ ψ
9 8 ad2antlr ⊢ Y ∈ Z ∧ Y ⁡ 0 = P ∧ w ∈ X → φ ∧ ψ ↔ φ ∧ Y ⁡ 0 = P ∧ ψ
10 9 rabbidva ⊢ Y ∈ Z ∧ Y ⁡ 0 = P → w ∈ X | φ ∧ ψ = w ∈ X | φ ∧ Y ⁡ 0 = P ∧ ψ
11 3 10 sylbi ⊢ Y ∈ w ∈ Z | w ⁡ 0 = P → w ∈ X | φ ∧ ψ = w ∈ X | φ ∧ Y ⁡ 0 = P ∧ ψ