Description: Obsolete version of noel as of 11-Oct-2026. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | noelOLD | |- -. A e. (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nsb | |- ( A. y -. F. -> -. [ x / y ] F. ) |
|
| 2 | fal | |- -. F. |
|
| 3 | 1 2 | mpg | |- -. [ x / y ] F. |
| 4 | dfnul4 | |- (/) = { y | F. } |
|
| 5 | 4 | eleq2i | |- ( x e. (/) <-> x e. { y | F. } ) |
| 6 | df-clab | |- ( x e. { y | F. } <-> [ x / y ] F. ) |
|
| 7 | 5 6 | bitri | |- ( x e. (/) <-> [ x / y ] F. ) |
| 8 | 3 7 | mtbir | |- -. x e. (/) |
| 9 | 8 | intnan | |- -. ( x = A /\ x e. (/) ) |
| 10 | 9 | nex | |- -. E. x ( x = A /\ x e. (/) ) |
| 11 | dfclel | |- ( A e. (/) <-> E. x ( x = A /\ x e. (/) ) ) |
|
| 12 | 10 11 | mtbir | |- -. A e. (/) |