Description: Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfabdw when possible. (Contributed by Mario Carneiro, 8-Oct-2016) Avoid ax-9 and ax-ext . (Revised by Wolf Lammen, 23-May-2023) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfabd.1 | |- F/ y ph |
|
| nfabd.2 | |- ( ph -> F/ x ps ) |
||
| Assertion | nfabd | |- ( ph -> F/_ x { y | ps } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfabd.1 | |- F/ y ph |
|
| 2 | nfabd.2 | |- ( ph -> F/ x ps ) |
|
| 3 | nfv | |- F/ z ph |
|
| 4 | df-clab | |- ( z e. { y | ps } <-> [ z / y ] ps ) |
|
| 5 | 1 2 | nfsbd | |- ( ph -> F/ x [ z / y ] ps ) |
| 6 | 4 5 | nfxfrd | |- ( ph -> F/ x z e. { y | ps } ) |
| 7 | 3 6 | nfcd | |- ( ph -> F/_ x { y | ps } ) |