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

Metamath Proof Explorer

Theorem equvinv

Description: A variable introduction law for equality. Lemma 15 of Monk2 p. 109. (Contributed by NM, 9-Jan-1993) Remove dependencies on ax-10 , ax-13 . (Revised by Wolf Lammen, 10-Jun-2019) Move the quantified variable ( z ) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021) (Proof shortened by Wolf Lammen, 12-Jul-2022)

		Ref	Expression
	Assertion	equvinv	⊢ ( 𝑥 = 𝑦 ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		equequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 = 𝑦 ↔ 𝑥 = 𝑦 ) )
2	1	equsexvw	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 = 𝑦 ) ↔ 𝑥 = 𝑦 )
3	2	bicomi	⊢ ( 𝑥 = 𝑦 ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 = 𝑦 ) )