This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nd4

Description: A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (New usage is discouraged.)

		Ref	Expression
	Assertion	nd4	$⊢ \forall x x = y \to \neg \forall z y \in x$

Proof

Step	Hyp	Ref	Expression
1		nd3	$⊢ \forall y y = x \to \neg \forall z y \in x$
2	1	aecoms	$⊢ \forall x x = y \to \neg \forall z y \in x$