Description: Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 16-Nov-2019) Avoid ax-12 . (Revised by Wolf Lammen, 19-Jun-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nfceqi.1 | |- A = B |
|
| Assertion | nfceqi | |- ( F/_ x A <-> F/_ x B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfceqi.1 | |- A = B |
|
| 2 | 1 | eleq2i | |- ( y e. A <-> y e. B ) |
| 3 | 2 | nfbii | |- ( F/ x y e. A <-> F/ x y e. B ) |
| 4 | 3 | albii | |- ( A. y F/ x y e. A <-> A. y F/ x y e. B ) |
| 5 | df-nfc | |- ( F/_ x A <-> A. y F/ x y e. A ) |
|
| 6 | df-nfc | |- ( F/_ x B <-> A. y F/ x y e. B ) |
|
| 7 | 4 5 6 | 3bitr4i | |- ( F/_ x A <-> F/_ x B ) |