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	⊢ ( { 𝑥 ∣ 𝜓 } ∈ 𝑉 → ( { 𝑥 ∣ 𝜓 } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ↔ ( { 𝑥 ∣ 𝜓 } ∈ { 𝑥 ∣ 𝜓 } → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜓 }
2	1 1	nfel	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜓 } ∈ { 𝑥 ∣ 𝜓 }
3		nfv	⊢ Ⅎ 𝑥 𝜑
4	2 3	nfim	⊢ Ⅎ 𝑥 ( { 𝑥 ∣ 𝜓 } ∈ { 𝑥 ∣ 𝜓 } → 𝜑 )
5		id	⊢ ( 𝑥 = { 𝑥 ∣ 𝜓 } → 𝑥 = { 𝑥 ∣ 𝜓 } )
6	5 5	eleq12d	⊢ ( 𝑥 = { 𝑥 ∣ 𝜓 } → ( 𝑥 ∈ 𝑥 ↔ { 𝑥 ∣ 𝜓 } ∈ { 𝑥 ∣ 𝜓 } ) )
7	6	imbi1d	⊢ ( 𝑥 = { 𝑥 ∣ 𝜓 } → ( ( 𝑥 ∈ 𝑥 → 𝜑 ) ↔ ( { 𝑥 ∣ 𝜓 } ∈ { 𝑥 ∣ 𝜓 } → 𝜑 ) ) )
8	1 4 7	elabgf	⊢ ( { 𝑥 ∣ 𝜓 } ∈ 𝑉 → ( { 𝑥 ∣ 𝜓 } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ↔ ( { 𝑥 ∣ 𝜓 } ∈ { 𝑥 ∣ 𝜓 } → 𝜑 ) ) )