theorem rappss (A B: set) (a: nat): $ A C_ B -> A @' a C_ B @' a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel | A C_ B -> a, a1 e. A -> a, a1 e. B |
|
2 | 1 | ssabd | A C_ B -> {a1 | a, a1 e. A} C_ {a1 | a, a1 e. B} |
3 | 2 | conv rapp | A C_ B -> A @' a C_ B @' a |