theorem coeqd (_G: wff) (_F1 _F2 _G1 _G2: set):
$ _G -> _F1 == _F2 $ >
$ _G -> _G1 == _G2 $ >
$ _G -> _F1 o> _G1 == _F2 o> _G2 $;
Step | Hyp | Ref | Expression |
1 |
|
eqidd |
_G -> x, y = x, y |
2 |
|
hyp _Fh |
_G -> _F1 == _F2 |
3 |
1, 2 |
eleqd |
_G -> (x, y e. _F1 <-> x, y e. _F2) |
4 |
|
eqidd |
_G -> y, z = y, z |
5 |
|
hyp _Gh |
_G -> _G1 == _G2 |
6 |
4, 5 |
eleqd |
_G -> (y, z e. _G1 <-> y, z e. _G2) |
7 |
3, 6 |
aneqd |
_G -> (x, y e. _F1 /\ y, z e. _G1 <-> x, y e. _F2 /\ y, z e. _G2) |
8 |
7 |
exeqd |
_G -> (E. y (x, y e. _F1 /\ y, z e. _G1) <-> E. y (x, y e. _F2 /\ y, z e. _G2)) |
9 |
8 |
abeqd |
_G -> {z | E. y (x, y e. _F1 /\ y, z e. _G1)} == {z | E. y (x, y e. _F2 /\ y, z e. _G2)} |
10 |
9 |
sabeqd |
_G -> S\ x, {z | E. y (x, y e. _F1 /\ y, z e. _G1)} == S\ x, {z | E. y (x, y e. _F2 /\ y, z e. _G2)} |
11 |
10 |
conv comp |
_G -> _F1 o> _G1 == _F2 o> _G2 |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp,
itru),
axs_pred_calc
(ax_gen,
ax_4,
ax_5,
ax_6,
ax_7,
ax_10,
ax_11,
ax_12),
axs_set
(elab,
ax_8)