theorem sabssi {x: nat} (A B: set x): $ A C_ B $ > $ S\ x, A C_ S\ x, B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sabss | S\ x, A C_ S\ x, B <-> A. x A C_ B |
|
2 | hyp h | A C_ B |
|
3 | 2 | ax_gen | A. x A C_ B |
4 | 1, 3 | mpbir | S\ x, A C_ S\ x, B |