Definition df-bnj15 29283

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 29282	. 2 wff R FrSe A
4	1, 2	wfr 4801	. . 3 wff R Fr A
5	1, 2	w-bnj13 29280	. . 3 wff R Se A
6	4, 5	wa 370	. 2 wff ( R Fr A /\ R Se A )
7	3, 6	wb 187	1 wff ( R FrSe A <-> ( R Fr A /\ R Se A ) )

This definition is referenced by:  bnj93  29459  bnj1177  29600  bnj1364  29622  bnj1417  29635