theorem nfsbid (G: wff) {x: nat} (A B: set x):
$ G -> A == B $ >
$ G -> ((FS/ x A) <-> (FS/ x B)) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | G -> A == B |
|
| 2 | 1 | eleq2d | G -> (y e. A <-> y e. B) |
| 3 | 2 | nfeqd | G -> ((F/ x y e. A) <-> (F/ x y e. B)) |
| 4 | 3 | aleqd | G -> (A. y (F/ x y e. A) <-> A. y (F/ x y e. B)) |
| 5 | 4 | conv nfs | G -> ((FS/ x A) <-> (FS/ x B)) |