Metamath Proof Explorer


Theorem bnj96

Description: Technical lemma for bnj150 . 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) (Revised by Mario Carneiro, 6-May-2015) (New usage is discouraged.)

Ref Expression
Hypothesis bnj96.1
|- F = { <. (/) , _pred ( x , A , R ) >. }
Assertion bnj96
|- ( ( R _FrSe A /\ x e. A ) -> dom F = 1o )

Proof

Step Hyp Ref Expression
1 bnj96.1
 |-  F = { <. (/) , _pred ( x , A , R ) >. }
2 bnj93
 |-  ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) e. _V )
3 dmsnopg
 |-  ( _pred ( x , A , R ) e. _V -> dom { <. (/) , _pred ( x , A , R ) >. } = { (/) } )
4 2 3 syl
 |-  ( ( R _FrSe A /\ x e. A ) -> dom { <. (/) , _pred ( x , A , R ) >. } = { (/) } )
5 1 dmeqi
 |-  dom F = dom { <. (/) , _pred ( x , A , R ) >. }
6 df1o2
 |-  1o = { (/) }
7 4 5 6 3eqtr4g
 |-  ( ( R _FrSe A /\ x e. A ) -> dom F = 1o )