Definition df-bnj15 29547

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.)

Assertion

Ref	Expression
df-bnj15	|- ( R FrSe A <-> ( R Fr A /\ R Se A ) )

Detailed syntax breakdown of Definition df-bnj15

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	w-bnj15 29546	. 2 wff R FrSe A
4	1, 2	wfr 4809	. . 3 wff R Fr A
5	1, 2	w-bnj13 29544	. . 3 wff R Se A
6	4, 5	wa 375	. 2 wff ( R Fr A /\ R Se A )
7	3, 6	wb 189	1 wff ( R FrSe A <-> ( R Fr A /\ R Se A ) )

This definition is referenced by:  bnj93  29723  bnj1177  29864  bnj1364  29886  bnj1417  29899