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 φ f = pred x A R
bnj118.2 No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
Assertion bnj118 Could not format assertion : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj118.1 φ f = pred x A R
2 bnj118.2 Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
3 bnj105 1 𝑜 V
4 1 3 bnj91 [˙ 1 𝑜 / n]˙ φ f = pred x A R
5 2 4 bitri Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-