Definition df-bnj15 35091

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 35090	. 2 wff 𝑅 FrSe 𝐴
4	1, 2	wfr 5610	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	w-bnj13 35088	. . 3 wff 𝑅 Se 𝐴
6	4, 5	wa 400	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴)
7	3, 6	wb 209	1 wff (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴))

This definition is used by:  bnj93  35260  bnj1177  35403  bnj1364  35425  bnj1417  35438