Metamath Proof Explorer

Theorem bnj91

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

Ref Expression
Hypotheses bnj91.1 
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj91.2 
|- Z e. _V
Assertion bnj91 
|- ( [. Z / y ]. ph <-> ( f ` (/) ) = _pred ( x , A , R ) )

Proof

Step Hyp Ref Expression
1 bnj91.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj91.2 
 |-  Z e. _V
3 1 sbcbii 
 |-  ( [. Z / y ]. ph <-> [. Z / y ]. ( f ` (/) ) = _pred ( x , A , R ) )
4 2 bnj525 
 |-  ( [. Z / y ]. ( f ` (/) ) = _pred ( x , A , R ) <-> ( f ` (/) ) = _pred ( x , A , R ) )
5 3 4 bitri 
 |-  ( [. Z / y ]. ph <-> ( f ` (/) ) = _pred ( x , A , R ) )