Theorem bnj219

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

	Ref	Expression
Assertion	bnj219	$$⊢n=\mathrm{suc}m\to m\mathrm{E}n$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢m\in \mathrm{V}$$
2	1	bnj216	$$⊢n=\mathrm{suc}m\to m\in n$$
3		epel	$$⊢m\mathrm{E}n\leftrightarrow m\in n$$
4	2 3	sylibr	$$⊢n=\mathrm{suc}m\to m\mathrm{E}n$$