Theorem ax6

Description: Theorem showing that ax-6 follows from the weaker version ax6v . (Even though this theorem depends on ax-6 , all references of ax-6 are made via ax6v . An earlier version stated ax6v as a separate axiom, but having two axioms caused some confusion.)

This theorem should be referenced in place of ax-6 so that all proofs can be traced back to ax6v . When possible, use the weaker ax6v rather than ax6 since the ax6v derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013) (Revised by NM, 25-Jul-2015) (Proof shortened by Wolf Lammen, 4-Feb-2018) Usage of this theorem is discouraged because it depends on ax-13 . Use ax6v instead. (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax6e	⊢ ∃ 𝑥 𝑥 = 𝑦
2		df-ex	⊢ ( ∃ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 )
3	1 2	mpbi	⊢ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦