Metamath Proof Explorer


Theorem bnj1083

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1083.3
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj1083.8
|- K = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
Assertion bnj1083
|- ( f e. K <-> E. n ch )

Proof

Step Hyp Ref Expression
1 bnj1083.3
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
2 bnj1083.8
 |-  K = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
3 df-rex
 |-  ( E. n e. D ( f Fn n /\ ph /\ ps ) <-> E. n ( n e. D /\ ( f Fn n /\ ph /\ ps ) ) )
4 2 abeq2i
 |-  ( f e. K <-> E. n e. D ( f Fn n /\ ph /\ ps ) )
5 bnj252
 |-  ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ ( f Fn n /\ ph /\ ps ) ) )
6 1 5 bitri
 |-  ( ch <-> ( n e. D /\ ( f Fn n /\ ph /\ ps ) ) )
7 6 exbii
 |-  ( E. n ch <-> E. n ( n e. D /\ ( f Fn n /\ ph /\ ps ) ) )
8 3 4 7 3bitr4i
 |-  ( f e. K <-> E. n ch )