Definition df-bnj15 30759

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 30758	. 2 wff R FrSe A
4	1, 2	wfr 5070	. . 3 wff R Fr A
5	1, 2	w-bnj13 30756	. . 3 wff R Se A
6	4, 5	wa 384	. 2 wff ( R Fr A /\ R Se A )
7	3, 6	wb 196	1 wff ( R FrSe A <-> ( R Fr A /\ R Se A ) )

This definition is referenced by:  bnj93  30933  bnj1177  31074  bnj1364  31096  bnj1417  31109