Theorem currysetlem2

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

	Ref	Expression
Hypothesis	currysetlem2.def	$$⊢X=\left\{x|\left(x\in x\to \phi \right)\right\}$$
Assertion	currysetlem2	$$⊢X\in V\to \left(X\in X\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		currysetlem2.def	$$⊢X=\left\{x|\left(x\in x\to \phi \right)\right\}$$
2	1	currysetlem1	$$⊢X\in V\to \left(X\in X\leftrightarrow \left(X\in X\to \phi \right)\right)$$
3	2	biimpd	$$⊢X\in V\to \left(X\in X\to \left(X\in X\to \phi \right)\right)$$
4	3	pm2.43d	$$⊢X\in V\to \left(X\in X\to \phi \right)$$