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

Metamath Proof Explorer

Theorem seeq12d

Description: Equality deduction for the set-like predicate. (Contributed by Matthew House, 10-Sep-2025)

	Ref	Expression
Hypotheses	seeq12d.1	$⊢ φ \to R = S$
	seeq12d.2	$⊢ φ \to A = B$
Assertion	seeq12d	$⊢ φ \to (R Se A \leftrightarrow S Se B)$

Step	Hyp	Ref	Expression
1		seeq12d.1	$⊢ φ \to R = S$
2		seeq12d.2	$⊢ φ \to A = B$
3		seeq1	$⊢ R = S \to (R Se A \leftrightarrow S Se A)$
4		seeq2	$⊢ A = B \to (S Se A \leftrightarrow S Se B)$
5	3 4	sylan9bb	$⊢ (R = S \land A = B) \to (R Se A \leftrightarrow S Se B)$
6	1 2 5	syl2anc	$⊢ φ \to (R Se A \leftrightarrow S Se B)$