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 | |- ( f ( W ` G ) p -> f ( Walks ` G ) p ) |
|
| Assertion | wlkResOLD | |- { <. f , p >. | ( f ( W ` G ) p /\ ph ) } e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlkResOLD.1 | |- ( f ( W ` G ) p -> f ( Walks ` G ) p ) |
|
| 2 | 1 | gen2 | |- A. f A. p ( f ( W ` G ) p -> f ( Walks ` G ) p ) |
| 3 | wksv | |- { <. f , p >. | f ( Walks ` G ) p } e. _V |
|
| 4 | opabbrex | |- ( ( A. f A. p ( f ( W ` G ) p -> f ( Walks ` G ) p ) /\ { <. f , p >. | f ( Walks ` G ) p } e. _V ) -> { <. f , p >. | ( f ( W ` G ) p /\ ph ) } e. _V ) |
|
| 5 | 2 3 4 | mp2an | |- { <. f , p >. | ( f ( W ` G ) p /\ ph ) } e. _V |