Theorem ax6vsep

Description: Derive ax6v (a weakened version of ax-6 where x and y must be distinct), from Separation ax-sep and Extensionality ax-ext . See ax6 for the derivation of ax-6 from ax6v . (Contributed by NM, 12-Nov-2013) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-sep	⊢ ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ( 𝑧 ∈ 𝑦 ∧ ( 𝑧 = 𝑧 → 𝑧 = 𝑧 ) ) )
2		id	⊢ ( 𝑧 = 𝑧 → 𝑧 = 𝑧 )
3	2	biantru	⊢ ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑦 ∧ ( 𝑧 = 𝑧 → 𝑧 = 𝑧 ) ) )
4	3	bibi2i	⊢ ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 ↔ ( 𝑧 ∈ 𝑦 ∧ ( 𝑧 = 𝑧 → 𝑧 = 𝑧 ) ) ) )
5	4	biimpri	⊢ ( ( 𝑧 ∈ 𝑥 ↔ ( 𝑧 ∈ 𝑦 ∧ ( 𝑧 = 𝑧 → 𝑧 = 𝑧 ) ) ) → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
6	5	alimi	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ( 𝑧 ∈ 𝑦 ∧ ( 𝑧 = 𝑧 → 𝑧 = 𝑧 ) ) ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
7		ax-ext	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )
8	6 7	syl	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ( 𝑧 ∈ 𝑦 ∧ ( 𝑧 = 𝑧 → 𝑧 = 𝑧 ) ) ) → 𝑥 = 𝑦 )
9	8	eximi	⊢ ( ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ( 𝑧 ∈ 𝑦 ∧ ( 𝑧 = 𝑧 → 𝑧 = 𝑧 ) ) ) → ∃ 𝑥 𝑥 = 𝑦 )
10	1 9	ax-mp	⊢ ∃ 𝑥 𝑥 = 𝑦
11		df-ex	⊢ ( ∃ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 )
12	10 11	mpbi	⊢ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦