Theorem rusgrnumwwlkslem

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

	Ref	Expression
Assertion	rusgrnumwwlkslem	⊢ ( 𝑌 ∈ { 𝑤 ∈ 𝑍 ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → { 𝑤 ∈ 𝑋 ∣ ( 𝜑 ∧ 𝜓 ) } = { 𝑤 ∈ 𝑋 ∣ ( 𝜑 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜓 ) } )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑤 = 𝑌 → ( 𝑤 ‘ 0 ) = ( 𝑌 ‘ 0 ) )
2	1	eqeq1d	⊢ ( 𝑤 = 𝑌 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑌 ‘ 0 ) = 𝑃 ) )
3	2	elrab	⊢ ( 𝑌 ∈ { 𝑤 ∈ 𝑍 ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ↔ ( 𝑌 ∈ 𝑍 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ) )
4		ibar	⊢ ( ( 𝑌 ‘ 0 ) = 𝑃 → ( ( 𝜑 ∧ 𝜓 ) ↔ ( ( 𝑌 ‘ 0 ) = 𝑃 ∧ ( 𝜑 ∧ 𝜓 ) ) ) )
5		3anass	⊢ ( ( ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜑 ∧ 𝜓 ) ↔ ( ( 𝑌 ‘ 0 ) = 𝑃 ∧ ( 𝜑 ∧ 𝜓 ) ) )
6		3ancoma	⊢ ( ( ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜓 ) )
7	5 6	bitr3i	⊢ ( ( ( 𝑌 ‘ 0 ) = 𝑃 ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( 𝜑 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜓 ) )
8	4 7	bitrdi	⊢ ( ( 𝑌 ‘ 0 ) = 𝑃 → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜓 ) ) )
9	8	ad2antlr	⊢ ( ( ( 𝑌 ∈ 𝑍 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜓 ) ) )
10	9	rabbidva	⊢ ( ( 𝑌 ∈ 𝑍 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ) → { 𝑤 ∈ 𝑋 ∣ ( 𝜑 ∧ 𝜓 ) } = { 𝑤 ∈ 𝑋 ∣ ( 𝜑 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜓 ) } )
11	3 10	sylbi	⊢ ( 𝑌 ∈ { 𝑤 ∈ 𝑍 ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → { 𝑤 ∈ 𝑋 ∣ ( 𝜑 ∧ 𝜓 ) } = { 𝑤 ∈ 𝑋 ∣ ( 𝜑 ∧ ( 𝑌 ‘ 0 ) = 𝑃 ∧ 𝜓 ) } )