Definition df-bnj15

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	w-bnj15	⊢ 𝑅 FrSe 𝐴
3	1 0	wfr	⊢ 𝑅 Fr 𝐴
4	1 0	w-bnj13	⊢ 𝑅 Se 𝐴
5	3 4	wa	⊢ ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 )
6	2 5	wb	⊢ ( 𝑅 FrSe 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) )