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

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