theorem sabssd (G: wff) {x: nat} (A B: set x):
$ G -> A C_ B $ >
$ G -> 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 | G -> A C_ B |
|
| 3 | 2 | iald | G -> A. x A C_ B |
| 4 | 1, 3 | sylibr | G -> S\ x, A C_ S\ x, B |