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

Metamath Proof Explorer

Theorem equidqe

Description: equid with existential quantifier without using ax-c5 or ax-5 . (Contributed by NM, 13-Jan-2011) (Proof shortened by Wolf Lammen, 27-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	equidqe	⊢ ¬ ∀ 𝑦 ¬ 𝑥 = 𝑥

Proof

Step	Hyp	Ref	Expression
1		ax6fromc10	⊢ ¬ ∀ 𝑦 ¬ 𝑦 = 𝑥
2		ax7	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝑥 → 𝑥 = 𝑥 ) )
3	2	pm2.43i	⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑥 )
4	3	con3i	⊢ ( ¬ 𝑥 = 𝑥 → ¬ 𝑦 = 𝑥 )
5	4	alimi	⊢ ( ∀ 𝑦 ¬ 𝑥 = 𝑥 → ∀ 𝑦 ¬ 𝑦 = 𝑥 )
6	1 5	mto	⊢ ¬ ∀ 𝑦 ¬ 𝑥 = 𝑥