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 = { x | ( x e. x -> ph ) }
Assertion	currysetlem1	|- ( X e. V -> ( X e. X <-> ( X e. X -> ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		currysetlem2.def	|- X = { x | ( x e. x -> ph ) }
2	1	eqcomi	|- { x | ( x e. x -> ph ) } = X
3	2	eleq2i	|- ( X e. { x | ( x e. x -> ph ) } <-> X e. X )
4		nfab1	|- F/_ x { x | ( x e. x -> ph ) }
5	1 4	nfcxfr	|- F/_ x X
6	5 5	nfel	|- F/ x X e. X
7		nfv	|- F/ x ph
8	6 7	nfim	|- F/ x ( X e. X -> ph )
9		id	|- ( x = X -> x = X )
10	9 9	eleq12d	|- ( x = X -> ( x e. x <-> X e. X ) )
11	10	imbi1d	|- ( x = X -> ( ( x e. x -> ph ) <-> ( X e. X -> ph ) ) )
12	5 8 11	elabgf	|- ( X e. V -> ( X e. { x | ( x e. x -> ph ) } <-> ( X e. X -> ph ) ) )
13	3 12	bitr3id	|- ( X e. V -> ( X e. X <-> ( X e. X -> ph ) ) )