Theorem axreg2

Description: Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003)

	Ref	Expression
Assertion	axreg2	$$⊢x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-reg	$$⊢\exists xx\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)$$
2	1	19.23bi	$$⊢x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)$$