theorem rappsabe (B: set) (a: nat) {x: nat} (A: set x): $ x = a -> A == B $ > $ (S\ x, A) @' a == B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | x = a -> A == B |
|
2 | 1 | anwr | T. /\ x = a -> A == B |
3 | 2 | rappsabed | T. -> (S\ x, A) @' a == B |
4 | 3 | trud | (S\ x, A) @' a == B |