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

Metamath Proof Explorer

Definition df-bnj19

Description: Define the following predicate: B is transitive for A and R . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-bnj19	$⊢ TrFo (B, A, R) \leftrightarrow \forall x \in B pred (x, A, R) \subseteq B$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cB	$class B$
1		cA	$class A$
2		cR	$class R$
3	1 0 2	w-bnj19	$wff TrFo (B, A, R)$
4		vx	$setvar x$
5	4	cv	$setvar x$
6	1 2 5	c-bnj14	$class pred (x, A, R)$
7	6 0	wss	$wff pred (x, A, R) \subseteq B$
8	7 4 0	wral	$wff \forall x \in B pred (x, A, R) \subseteq B$
9	3 8	wb	$wff (TrFo (B, A, R) \leftrightarrow \forall x \in B pred (x, A, R) \subseteq B)$