pm13.194

		Ref	Expression
	Assertion	pm13.194	$⊢ (φ \land x = y) \leftrightarrow ([y/ x] φ \land φ \land x = y)$

Step	Hyp	Ref	Expression
1		pm13.13a	$⊢ (φ \land x = y) \to \underset{˙}{[} y / x \underset{˙}{]} φ$
2		sbsbc	$⊢ [y/ x] φ \leftrightarrow \underset{˙}{[} y / x \underset{˙}{]} φ$
3	1 2	sylibr	$⊢ (φ \land x = y) \to [y/ x] φ$
4		simpl	$⊢ (φ \land x = y) \to φ$
5		simpr	$⊢ (φ \land x = y) \to x = y$
6	3 4 5	3jca	$⊢ (φ \land x = y) \to ([y/ x] φ \land φ \land x = y)$
7		3simpc	$⊢ ([y/ x] φ \land φ \land x = y) \to (φ \land x = y)$
8	6 7	impbii	$⊢ (φ \land x = y) \leftrightarrow ([y/ x] φ \land φ \land x = y)$

Metamath Proof Explorer