Metamath Proof Explorer


Theorem wlkResOLD

Description: Obsolete version of opabresex2 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 30-Dec-2020) (Proof shortened by AV, 15-Jan-2021) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis wlkResOLD.1 ( 𝑓 ( 𝑊𝐺 ) 𝑝𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
Assertion wlkResOLD { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑊𝐺 ) 𝑝𝜑 ) } ∈ V

Proof

Step Hyp Ref Expression
1 wlkResOLD.1 ( 𝑓 ( 𝑊𝐺 ) 𝑝𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
2 1 gen2 𝑓𝑝 ( 𝑓 ( 𝑊𝐺 ) 𝑝𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
3 wksv { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V
4 opabbrex ( ( ∀ 𝑓𝑝 ( 𝑓 ( 𝑊𝐺 ) 𝑝𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) ∧ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V ) → { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑊𝐺 ) 𝑝𝜑 ) } ∈ V )
5 2 3 4 mp2an { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑊𝐺 ) 𝑝𝜑 ) } ∈ V