Metamath Proof Explorer

Theorem currysetlem

Description: Lemma for currysetlem , where it is used with ( x e. x -> ph ) substituted for ps . (Contributed by BJ, 23-Sep-2023) This proof is intuitionistically valid. (Proof modification is discouraged.)

Ref Expression
Assertion currysetlem ⊢ x | ψ ∈ V → x | ψ ∈ x | x ∈ x → φ ↔ x | ψ ∈ x | ψ → φ

Proof

Step Hyp Ref Expression
1 nfab1 ⊢ Ⅎ _ x x | ψ
2 1 1 nfel ⊢ Ⅎ x x | ψ ∈ x | ψ
3 nfv ⊢ Ⅎ x φ
4 2 3 nfim ⊢ Ⅎ x x | ψ ∈ x | ψ → φ
5 id ⊢ x = x | ψ → x = x | ψ
6 5 5 eleq12d ⊢ x = x | ψ → x ∈ x ↔ x | ψ ∈ x | ψ
7 6 imbi1d ⊢ x = x | ψ → x ∈ x → φ ↔ x | ψ ∈ x | ψ → φ
8 1 4 7 elabgf ⊢ x | ψ ∈ V → x | ψ ∈ x | x ∈ x → φ ↔ x | ψ ∈ x | ψ → φ