predeq123

Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018)

		Ref	Expression
	Assertion	predeq123	$⊢ (R = S \land A = B \land X = Y) \to Pred (R, A, X) = Pred (S, B, Y)$

Step	Hyp	Ref	Expression
1		simp2	$⊢ (R = S \land A = B \land X = Y) \to A = B$
2		cnveq	$⊢ R = S \to R^{-1} = S^{-1}$
3	2	3ad2ant1	$⊢ (R = S \land A = B \land X = Y) \to R^{-1} = S^{-1}$
4		sneq	$⊢ X = Y \to \{X\} = \{Y\}$
5	4	3ad2ant3	$⊢ (R = S \land A = B \land X = Y) \to \{X\} = \{Y\}$
6	3 5	imaeq12d	$⊢ (R = S \land A = B \land X = Y) \to R^{-1} [\{X\}] = S^{-1} [\{Y\}]$
7	1 6	ineq12d	$⊢ (R = S \land A = B \land X = Y) \to A \cap R^{-1} [\{X\}] = B \cap S^{-1} [\{Y\}]$
8		df-pred	$⊢ Pred (R, A, X) = A \cap R^{-1} [\{X\}]$
9		df-pred	$⊢ Pred (S, B, Y) = B \cap S^{-1} [\{Y\}]$
10	7 8 9	3eqtr4g	$⊢ (R = S \land A = B \land X = Y) \to Pred (R, A, X) = Pred (S, B, Y)$

Metamath Proof Explorer