axextg

Description: A generalization of the axiom of extensionality in which x and y need not be distinct. (Contributed by NM, 15-Sep-1993) (Proof shortened by Andrew Salmon, 12-Aug-2011) Remove dependencies on ax-10 , ax-12 , ax-13 . (Revised by BJ, 12-Jul-2019) (Revised by Wolf Lammen, 9-Dec-2019)

		Ref	Expression
	Assertion	axextg	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		elequ2	⊢ ( 𝑤 = 𝑥 → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥 ) )
2	1	bibi1d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
3	2	albidv	⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
4		equequ1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 = 𝑦 ↔ 𝑥 = 𝑦 ) )
5	3 4	imbi12d	⊢ ( 𝑤 = 𝑥 → ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦 ) → 𝑤 = 𝑦 ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )
6		ax-ext	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦 ) → 𝑤 = 𝑦 )
7	5 6	chvarvv	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )

Metamath Proof Explorer

Theorem axextg

Proof