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	$$⊢X=\left\{x|\left(x\in x\to \phi \right)\right\}$$
Assertion	currysetlem1	$$⊢X\in V\to \left(X\in X\leftrightarrow \left(X\in X\to \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		currysetlem2.def	$$⊢X=\left\{x|\left(x\in x\to \phi \right)\right\}$$
2	1	eqcomi	$$⊢\left\{x|\left(x\in x\to \phi \right)\right\}=X$$
3	2	eleq2i	$$⊢X\in \left\{x|\left(x\in x\to \phi \right)\right\}\leftrightarrow X\in X$$
4		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\left(x\in x\to \phi \right)\right\}$$
5	1 4	nfcxfr	$$⊢\underset{\_}{Ⅎ}xX$$
6	5 5	nfel	$$⊢ℲxX\in X$$
7		nfv	$$⊢Ⅎx\phi$$
8	6 7	nfim	$$⊢Ⅎx\left(X\in X\to \phi \right)$$
9		id	$$⊢x=X\to x=X$$
10	9 9	eleq12d	$$⊢x=X\to \left(x\in x\leftrightarrow X\in X\right)$$
11	10	imbi1d	$$⊢x=X\to \left(\left(x\in x\to \phi \right)\leftrightarrow \left(X\in X\to \phi \right)\right)$$
12	5 8 11	elabgf	$$⊢X\in V\to \left(X\in \left\{x|\left(x\in x\to \phi \right)\right\}\leftrightarrow \left(X\in X\to \phi \right)\right)$$
13	3 12	bitr3id	$$⊢X\in V\to \left(X\in X\leftrightarrow \left(X\in X\to \phi \right)\right)$$