Description: Alternate version of nfcr . Avoids ax-8 but uses ax-12 . (Contributed by Mario Carneiro, 11-Aug-2016) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfcrALT | |- ( F/_ x A -> F/ x y e. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nfc | |- ( F/_ x A <-> A. y F/ x y e. A ) |
|
| 2 | sp | |- ( A. y F/ x y e. A -> F/ x y e. A ) |
|
| 3 | 1 2 | sylbi | |- ( F/_ x A -> F/ x y e. A ) |