theorem eqri2 (A B: set) {x y: nat}: $ x, y e. A <-> x, y e. B $ > $ A == B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | x, y e. A <-> x, y e. B |
|
2 | 1 | a1i | T. -> (x, y e. A <-> x, y e. B) |
3 | 2 | eqrd2 | T. -> A == B |
4 | 3 | trud | A == B |