Description: Obsolete version of nfceqdf as of 23-Aug-2024. (Contributed by Mario Carneiro, 14-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfceqdf.1 | |- F/ x ph |
|
| nfceqdf.2 | |- ( ph -> A = B ) |
||
| Assertion | nfceqdfOLD | |- ( ph -> ( F/_ x A <-> F/_ x B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfceqdf.1 | |- F/ x ph |
|
| 2 | nfceqdf.2 | |- ( ph -> A = B ) |
|
| 3 | 2 | eleq2d | |- ( ph -> ( y e. A <-> y e. B ) ) |
| 4 | 1 3 | nfbidf | |- ( ph -> ( F/ x y e. A <-> F/ x y e. B ) ) |
| 5 | 4 | albidv | |- ( ph -> ( A. y F/ x y e. A <-> A. y F/ x y e. B ) ) |
| 6 | df-nfc | |- ( F/_ x A <-> A. y F/ x y e. A ) |
|
| 7 | df-nfc | |- ( F/_ x B <-> A. y F/ x y e. B ) |
|
| 8 | 5 6 7 | 3bitr4g | |- ( ph -> ( F/_ x A <-> F/_ x B ) ) |