theorem nfeqs {x: nat} (A B: set x):
$ FS/ x A $ >
$ FS/ x B $ >
$ F/ x A == B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h1 | FS/ x A |
|
| 2 | 1 | nfel2 | F/ x y e. A |
| 3 | hyp h2 | FS/ x B |
|
| 4 | 3 | nfel2 | F/ x y e. B |
| 5 | 2, 4 | nfbi | F/ x y e. A <-> y e. B |
| 6 | 5 | nfal | F/ x A. y (y e. A <-> y e. B) |
| 7 | 6 | conv eqs | F/ x A == B |