Definition df-bnj15 32572

Description: Define the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Assertion

Ref	Expression
df-bnj15	⊢ (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴))

Detailed syntax breakdown of Definition df-bnj15

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	w-bnj15 32571	. 2 wff 𝑅 FrSe 𝐴
4	1, 2	wfr 5532	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	w-bnj13 32569	. . 3 wff 𝑅 Se 𝐴
6	4, 5	wa 395	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴)
7	3, 6	wb 205	1 wff (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴))

This definition is referenced by:  bnj93  32743  bnj1177  32886  bnj1364  32908  bnj1417  32921