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	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
2	1	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
3		vex	⊢ 𝑦 ∈ V
4	3	tz9.13	⊢ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 )
5	2 4	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )