axextprim

Description: ax-ext without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010)

		Ref	Expression
	Assertion	axextprim	$⊢ \neg \forall x \neg ((x \in y \to x \in z) \to ((x \in z \to x \in y) \to y = z))$

Step	Hyp	Ref	Expression
1		axextnd	$⊢ \exists x ((x \in y \leftrightarrow x \in z) \to y = z)$
2		dfbi2	$⊢ (x \in y \leftrightarrow x \in z) \leftrightarrow ((x \in y \to x \in z) \land (x \in z \to x \in y))$
3	2	imbi1i	$⊢ ((x \in y \leftrightarrow x \in z) \to y = z) \leftrightarrow (((x \in y \to x \in z) \land (x \in z \to x \in y)) \to y = z)$
4		impexp	$⊢ (((x \in y \to x \in z) \land (x \in z \to x \in y)) \to y = z) \leftrightarrow ((x \in y \to x \in z) \to ((x \in z \to x \in y) \to y = z))$
5	3 4	bitri	$⊢ ((x \in y \leftrightarrow x \in z) \to y = z) \leftrightarrow ((x \in y \to x \in z) \to ((x \in z \to x \in y) \to y = z))$
6	5	exbii	$⊢ \exists x ((x \in y \leftrightarrow x \in z) \to y = z) \leftrightarrow \exists x ((x \in y \to x \in z) \to ((x \in z \to x \in y) \to y = z))$
7		df-ex	$⊢ \exists x ((x \in y \to x \in z) \to ((x \in z \to x \in y) \to y = z)) \leftrightarrow \neg \forall x \neg ((x \in y \to x \in z) \to ((x \in z \to x \in y) \to y = z))$
8	6 7	bitri	$⊢ \exists x ((x \in y \leftrightarrow x \in z) \to y = z) \leftrightarrow \neg \forall x \neg ((x \in y \to x \in z) \to ((x \in z \to x \in y) \to y = z))$
9	1 8	mpbi	$⊢ \neg \forall x \neg ((x \in y \to x \in z) \to ((x \in z \to x \in y) \to y = z))$

Metamath Proof Explorer