Description: Version of nfsb2 with a disjoint variable condition, which does not require ax-13 , and removal of ax-13 from nfs1v . (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-nfs1v | |- F/ x [ y / x ] ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-hbs1 | |- ( [ y / x ] ph -> A. x [ y / x ] ph ) |
|
| 2 | 1 | nf5i | |- F/ x [ y / x ] ph |