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	|- ( R _FrSe A <-> ( R Fr A /\ R _Se A ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1		cA	|- A
2	1 0	w-bnj15	|- R _FrSe A
3	1 0	wfr	|- R Fr A
4	1 0	w-bnj13	|- R _Se A
5	3 4	wa	|- ( R Fr A /\ R _Se A )
6	2 5	wb	|- ( R _FrSe A <-> ( R Fr A /\ R _Se A ) )