Theorem currysetALT

Description: Alternate proof of curryset , or more precisely alternate exposal of the same proof. (Contributed by BJ, 23-Sep-2023) This proof is intuitionistically valid. (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	currysetALT	$$⊢\neg \left\{x|\left(x\in x\to \phi \right)\right\}\in V$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{x|\left(x\in x\to \phi \right)\right\}=\left\{x|\left(x\in x\to \phi \right)\right\}$$
2	1	currysetlem3	$$⊢\neg \left\{x|\left(x\in x\to \phi \right)\right\}\in V$$