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

Metamath Proof Explorer

Theorem equvini

Description: A variable introduction law for equality. Lemma 15 of Monk2 p. 109, however we do not require z to be distinct from x and y . Usage of this theorem is discouraged because it depends on ax-13 . See equvinv for a shorter proof requiring fewer axioms when z is required to be distinct from x and y . (Contributed by NM, 10-Jan-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 16-Sep-2023) (New usage is discouraged.)

Ref Expression
Assertion equvini ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 equtr ⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) )
2 equcomi ⊢ ( 𝑧 = 𝑥 → 𝑥 = 𝑧 )
3 1 2 jctild ⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) )
4 19.8a ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )
5 3 4 syl6 ⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) )
6 ax13 ⊢ ( ¬ 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
7 ax6e ⊢ ∃ 𝑧 𝑧 = 𝑥
8 7 3 eximii ⊢ ∃ 𝑧 ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )
9 8 19.35i ⊢ ( ∀ 𝑧 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )
10 6 9 syl6 ⊢ ( ¬ 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) )
11 5 10 pm2.61i ⊢ ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )