Definition df-bnj15 32825

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 32824	. 2 wff R FrSe A
4	1, 2	wfr 4835	. . 3 wff R Fr A
5	1, 2	w-bnj13 32822	. . 3 wff R Se A
6	4, 5	wa 369	. 2 wff ( R Fr A /\ R Se A )
7	3, 6	wb 184	1 wff ( R FrSe A <-> ( R Fr A /\ R Se A ) )

This definition is referenced by:  bnj93  33000  bnj1177  33141  bnj1364  33163  bnj1417  33176