theorem nfel2 {x: nat} (a: nat) (A: set x): $ FS/ x A $ > $ F/ x a e. A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1 | y = a -> (y e. A <-> a e. A) |
|
| 2 | 1 | nfeqd | y = a -> ((F/ x y e. A) <-> (F/ x a e. A)) |
| 3 | 2 | eale | A. y (F/ x y e. A) -> (F/ x a e. A) |
| 4 | hyp h | FS/ x A |
|
| 5 | 4 | conv nfs | A. y (F/ x y e. A) |
| 6 | 3, 5 | ax_mp | F/ x a e. A |