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

Metamath Proof Explorer

Theorem bnj602

Description: Equality theorem for the _pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj602	$⊢ X = Y \to pred (X, A, R) = pred (Y, A, R)$

Step	Hyp	Ref	Expression
1		breq2	$⊢ X = Y \to (y R X \leftrightarrow y R Y)$
2	1	rabbidv	$⊢ X = Y \to \{y \in A \| y R X\} = \{y \in A \| y R Y\}$
3		df-bnj14	$⊢ pred (X, A, R) = \{y \in A \| y R X\}$
4		df-bnj14	$⊢ pred (Y, A, R) = \{y \in A \| y R Y\}$
5	2 3 4	3eqtr4g	$⊢ X = Y \to pred (X, A, R) = pred (Y, A, R)$