Metamath Proof Explorer


Theorem bnj118

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj118.1
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj118.2
|- ( ph' <-> [. 1o / n ]. ph )
Assertion bnj118
|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )

Proof

Step Hyp Ref Expression
1 bnj118.1
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj118.2
 |-  ( ph' <-> [. 1o / n ]. ph )
3 bnj105
 |-  1o e. _V
4 1 3 bnj91
 |-  ( [. 1o / n ]. ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
5 2 4 bitri
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )