Metamath Proof Explorer

Theorem currysetlem

Description: Lemma for currysetlem , where it is used with ( x e. x -> ph ) substituted for ps . (Contributed by BJ, 23-Sep-2023) This proof is intuitionistically valid. (Proof modification is discouraged.)

Ref Expression
Assertion currysetlem 
|- ( { x | ps } e. V -> ( { x | ps } e. { x | ( x e. x -> ph ) } <-> ( { x | ps } e. { x | ps } -> ph ) ) )

Proof

Step Hyp Ref Expression
1 nfab1 
 |-  F/_ x { x | ps }
2 1 1 nfel 
 |-  F/ x { x | ps } e. { x | ps }
3 nfv 
 |-  F/ x ph
4 2 3 nfim 
 |-  F/ x ( { x | ps } e. { x | ps } -> ph )
5 id 
 |-  ( x = { x | ps } -> x = { x | ps } )
6 5 5 eleq12d 
 |-  ( x = { x | ps } -> ( x e. x <-> { x | ps } e. { x | ps } ) )
7 6 imbi1d 
 |-  ( x = { x | ps } -> ( ( x e. x -> ph ) <-> ( { x | ps } e. { x | ps } -> ph ) ) )
8 1 4 7 elabgf 
 |-  ( { x | ps } e. V -> ( { x | ps } e. { x | ( x e. x -> ph ) } <-> ( { x | ps } e. { x | ps } -> ph ) ) )