Definition df-bnj15 34707

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 34706	. 2 wff 𝑅 FrSe 𝐴
4	1, 2	wfr 5634	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	w-bnj13 34704	. . 3 wff 𝑅 Se 𝐴
6	4, 5	wa 395	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴)
7	3, 6	wb 206	1 wff (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴))

This definition is referenced by:  bnj93  34877  bnj1177  35020  bnj1364  35042  bnj1417  35055