bnj1414

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	bnj1414.1	$⊢ B = pred (X, A, R) \cup ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
	Assertion	bnj1414	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) = B$

Step	Hyp	Ref	Expression
1		bnj1414.1	$⊢ B = pred (X, A, R) \cup ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
2		eqid	$⊢ pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) = pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
3		biid	$⊢ (R FrSe A \land X \in A) \leftrightarrow (R FrSe A \land X \in A)$
4		biid	$⊢ (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B) \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
5	1 2 3 4	bnj1408	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) = B$

Metamath Proof Explorer