Metamath Proof Explorer


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 x φ
Assertion currysetlem1 X V X X X X φ

Proof

Step Hyp Ref Expression
1 currysetlem2.def X = x | x x φ
2 1 eqcomi x | x x φ = X
3 2 eleq2i X x | x x φ X X
4 nfab1 _ x x | x x φ
5 1 4 nfcxfr _ x X
6 5 5 nfel x X X
7 nfv x φ
8 6 7 nfim x X X φ
9 id x = X x = X
10 9 9 eleq12d x = X x x X X
11 10 imbi1d x = X x x φ X X φ
12 5 8 11 elabgf X V X x | x x φ X X φ
13 3 12 bitr3id X V X X X X φ