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	$⊢ \forall z (z \in x \leftrightarrow z \in y) \to x = y$

Proof

Step	Hyp	Ref	Expression
1		elequ2	$⊢ w = x \to (z \in w \leftrightarrow z \in x)$
2	1	bibi1d	$⊢ w = x \to ((z \in w \leftrightarrow z \in y) \leftrightarrow (z \in x \leftrightarrow z \in y))$
3	2	albidv	$⊢ w = x \to (\forall z (z \in w \leftrightarrow z \in y) \leftrightarrow \forall z (z \in x \leftrightarrow z \in y))$
4		equequ1	$⊢ w = x \to (w = y \leftrightarrow x = y)$
5	3 4	imbi12d	$⊢ w = x \to ((\forall z (z \in w \leftrightarrow z \in y) \to w = y) \leftrightarrow (\forall z (z \in x \leftrightarrow z \in y) \to x = y))$
6		ax-ext	$⊢ \forall z (z \in w \leftrightarrow z \in y) \to w = y$
7	5 6	chvarvv	$⊢ \forall z (z \in x \leftrightarrow z \in y) \to x = y$

Metamath Proof Explorer

Theorem axextg

Proof