theorem sappslame (B: set) (a: nat) {x: nat} (A: set x): $ x = a -> A == B $ > $ (\\ 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 | sappslamed | T. -> (\\ x, A) @@ a == B |
4 | 3 | trud | (\\ x, A) @@ a == B |