Definition df-bnj15

Description: Define the following predicate: R is both well-founded and set-like on A . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bnj15	$$⊢RFrSeA\leftrightarrow \left(R\mathrm{Fr}A\wedge RSeA\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	w-bnj15	$$wffRFrSeA$$
3	1 0	wfr	$$wffR\mathrm{Fr}A$$
4	1 0	w-bnj13	$$wffRSeA$$
5	3 4	wa	$$wff\left(R\mathrm{Fr}A\wedge RSeA\right)$$
6	2 5	wb	$$wff\left(RFrSeA\leftrightarrow \left(R\mathrm{Fr}A\wedge RSeA\right)\right)$$