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

Proof

Step	Hyp	Ref	Expression
1		currysetlem2.def	|- X = { x | ( x e. x -> ph ) }
2	1	currysetlem1	|- ( X e. V -> ( X e. X <-> ( X e. X -> ph ) ) )
3	2	biimpd	|- ( X e. V -> ( X e. X -> ( X e. X -> ph ) ) )
4	3	pm2.43d	|- ( X e. V -> ( X e. X -> ph ) )