Definition df-bnj15 30759

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 30758	. 2 wff 𝑅 FrSe 𝐴
4	1, 2	wfr 5070	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	w-bnj13 30756	. . 3 wff 𝑅 Se 𝐴
6	4, 5	wa 384	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴)
7	3, 6	wb 196	1 wff (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴))

This definition is referenced by:  bnj93  30933  bnj1177  31074  bnj1364  31096  bnj1417  31109