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 e. V -> E. x e. On A e. ( R1 ` x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1 | |- ( y = A -> ( y e. ( R1 ` x ) <-> A e. ( R1 ` x ) ) ) |
|
| 2 | 1 | rexbidv | |- ( y = A -> ( E. x e. On y e. ( R1 ` x ) <-> E. x e. On A e. ( R1 ` x ) ) ) |
| 3 | vex | |- y e. _V |
|
| 4 | 3 | tz9.13 | |- E. x e. On y e. ( R1 ` x ) |
| 5 | 2 4 | vtoclg | |- ( A e. V -> E. x e. On A e. ( R1 ` x ) ) |