Description: An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016) Avoid ax-8 and df-clel . (Revised by WL and SN, 23-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfceqdf.1 | |- F/ x ph |
|
| nfceqdf.2 | |- ( ph -> A = B ) |
||
| Assertion | nfceqdf | |- ( ph -> ( F/_ x A <-> F/_ x B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfceqdf.1 | |- F/ x ph |
|
| 2 | nfceqdf.2 | |- ( ph -> A = B ) |
|
| 3 | eleq2w2 | |- ( A = B -> ( y e. A <-> y e. B ) ) |
|
| 4 | 2 3 | syl | |- ( ph -> ( y e. A <-> y e. B ) ) |
| 5 | 1 4 | nfbidf | |- ( ph -> ( F/ x y e. A <-> F/ x y e. B ) ) |
| 6 | 5 | albidv | |- ( ph -> ( A. y F/ x y e. A <-> A. y F/ x y e. B ) ) |
| 7 | df-nfc | |- ( F/_ x A <-> A. y F/ x y e. A ) |
|
| 8 | df-nfc | |- ( F/_ x B <-> A. y F/ x y e. B ) |
|
| 9 | 6 7 8 | 3bitr4g | |- ( ph -> ( F/_ x A <-> F/_ x B ) ) |