theorem writeeqd (_G: wff) (_F1 _F2: set) (_a1 _a2 _b1 _b2: nat): $ _G -> _F1 == _F2 $ > $ _G -> _a1 = _a2 $ > $ _G -> _b1 = _b2 $ > $ _G -> write _F1 _a1 _b1 == write _F2 _a2 _b2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 |
_G -> x = x |
||
2 |
hyp _ah |
_G -> _a1 = _a2 |
|
3 |
_G -> (x = _a1 <-> x = _a2) |
||
4 |
_G -> y = y |
||
5 |
hyp _bh |
_G -> _b1 = _b2 |
|
6 |
_G -> (y = _b1 <-> y = _b2) |
||
7 |
_G -> x, y = x, y |
||
8 |
hyp _Fh |
_G -> _F1 == _F2 |
|
9 |
_G -> (x, y e. _F1 <-> x, y e. _F2) |
||
10 |
_G -> (ifp (x = _a1) (y = _b1) (x, y e. _F1) <-> ifp (x = _a2) (y = _b2) (x, y e. _F2)) |
||
11 |
_G -> {y | ifp (x = _a1) (y = _b1) (x, y e. _F1)} == {y | ifp (x = _a2) (y = _b2) (x, y e. _F2)} |
||
12 |
_G -> S\ x, {y | ifp (x = _a1) (y = _b1) (x, y e. _F1)} == S\ x, {y | ifp (x = _a2) (y = _b2) (x, y e. _F2)} |
||
13 |
conv write |
_G -> write _F1 _a1 _b1 == write _F2 _a2 _b2 |