Metamath Proof Explorer

Theorem tz9.13g

Description: Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of TakeutiZaring p. 78. This variant of tz9.13 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003)

		Ref	Expression
	Assertion	tz9.13g	$⊢ A \in V \to \exists x \in On A \in R_{1} (x)$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ y = A \to (y \in R_{1} (x) \leftrightarrow A \in R_{1} (x))$
2	1	rexbidv	$⊢ y = A \to (\exists x \in On y \in R_{1} (x) \leftrightarrow \exists x \in On A \in R_{1} (x))$
3		vex	$⊢ y \in V$
4	3	tz9.13	$⊢ \exists x \in On y \in R_{1} (x)$
5	2 4	vtoclg	$⊢ A \in V \to \exists x \in On A \in R_{1} (x)$