Definition df-bnj15 31956

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 31955	. 2 wff 𝑅 FrSe 𝐴
4	1, 2	wfr 5504	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	w-bnj13 31953	. . 3 wff 𝑅 Se 𝐴
6	4, 5	wa 398	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴)
7	3, 6	wb 208	1 wff (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴))

This definition is referenced by:  bnj93  32128  bnj1177  32271  bnj1364  32293  bnj1417  32306