This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ R FrSe A \leftrightarrow (R Fr A \land R Se A)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1		cA	$class A$
2	1 0	w-bnj15	$wff R FrSe A$
3	1 0	wfr	$wff R Fr A$
4	1 0	w-bnj13	$wff R Se A$
5	3 4	wa	$wff (R Fr A \land R Se A)$
6	2 5	wb	$wff (R FrSe A \leftrightarrow (R Fr A \land R Se A))$