This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cusgrexilem1

Description: Lemma 1 for cusgrexi . (Contributed by Alexander van der Vekens, 12-Jan-2018)

Ref Expression
Hypothesis usgrexi.p ⊢ P = x ∈ 𝒫 V | x = 2
Assertion cusgrexilem1 ⊢ V ∈ W → I ↾ P ∈ V

Proof

Step Hyp Ref Expression
1 usgrexi.p ⊢ P = x ∈ 𝒫 V | x = 2
2 pwexg ⊢ V ∈ W → 𝒫 V ∈ V
3 1 2 rabexd ⊢ V ∈ W → P ∈ V
4 resiexg ⊢ P ∈ V → I ↾ P ∈ V
5 3 4 syl ⊢ V ∈ W → I ↾ P ∈ V