theorem inv2 (A: set): $ A i^i _V == A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqstr | A i^i _V == _V i^i A -> _V i^i A == A -> A i^i _V == A |
|
2 | incom | A i^i _V == _V i^i A |
|
3 | 1, 2 | ax_mp | _V i^i A == A -> A i^i _V == A |
4 | inv1 | _V i^i A == A |
|
5 | 3, 4 | ax_mp | A i^i _V == A |