theorem nfsab1 {x: nat} (A: set x): $ FS/ x S\ x, A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfsbs1 | FS/ x S[fst a1 / x] A |
|
2 | 1 | nfel2 | F/ x snd a1 e. S[fst a1 / x] A |
3 | 2 | nfab | FS/ x {a1 | snd a1 e. S[fst a1 / x] A} |
4 | 3 | conv sab | FS/ x S\ x, A |