Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by NM, 14-Oct-2010) (Revised by Mario Carneiro, 18-Nov-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eusv2i | |- ( E! y A. x y = A -> E! y E. x y = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfeu1 | |- F/ y E! y A. x y = A |
|
| 2 | nfcvd | |- ( E! y A. x y = A -> F/_ x y ) |
|
| 3 | eusvnf | |- ( E! y A. x y = A -> F/_ x A ) |
|
| 4 | 2 3 | nfeqd | |- ( E! y A. x y = A -> F/ x y = A ) |
| 5 | 4 | nfrd | |- ( E! y A. x y = A -> ( E. x y = A -> A. x y = A ) ) |
| 6 | 19.2 | |- ( A. x y = A -> E. x y = A ) |
|
| 7 | 5 6 | impbid1 | |- ( E! y A. x y = A -> ( E. x y = A <-> A. x y = A ) ) |
| 8 | 1 7 | eubid | |- ( E! y A. x y = A -> ( E! y E. x y = A <-> E! y A. x y = A ) ) |
| 9 | 8 | ibir | |- ( E! y A. x y = A -> E! y E. x y = A ) |