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 ) )