Theorem currysetlem1

Description: Lemma for currysetALT . (Contributed by BJ, 23-Sep-2023) This proof is intuitionistically valid. (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	currysetlem2.def	⊢ 𝑋 = { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) }
Assertion	currysetlem1	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ 𝑋 ↔ ( 𝑋 ∈ 𝑋 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		currysetlem2.def	⊢ 𝑋 = { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) }
2	1	eqcomi	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } = 𝑋
3	2	eleq2i	⊢ ( 𝑋 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ↔ 𝑋 ∈ 𝑋 )
4		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) }
5	1 4	nfcxfr	⊢ Ⅎ 𝑥 𝑋
6	5 5	nfel	⊢ Ⅎ 𝑥 𝑋 ∈ 𝑋
7		nfv	⊢ Ⅎ 𝑥 𝜑
8	6 7	nfim	⊢ Ⅎ 𝑥 ( 𝑋 ∈ 𝑋 → 𝜑 )
9		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
10	9 9	eleq12d	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝑥 ↔ 𝑋 ∈ 𝑋 ) )
11	10	imbi1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝑥 → 𝜑 ) ↔ ( 𝑋 ∈ 𝑋 → 𝜑 ) ) )
12	5 8 11	elabgf	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ↔ ( 𝑋 ∈ 𝑋 → 𝜑 ) ) )
13	3 12	bitr3id	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ 𝑋 ↔ ( 𝑋 ∈ 𝑋 → 𝜑 ) ) )