Theorem ocasepeqd ≪ | index | src | ≫

theorem ocasepeqd (_G _z1 _z2: wff) (_S1 _S2: set):
  $ _G -> (_z1 <-> _z2) $ >
  $ _G -> _S1 == _S2 $ >
  $ _G -> ocasep _z1 _S1 == ocasep _z2 _S2 $;

Step	Hyp	Ref	Expression
1		biidd	_G -> (n = 0 <-> n = 0)
2		hyp _zh	_G -> (_z1 <-> _z2)
3		eqidd	_G -> n - 1 = n - 1
4		hyp _Sh	_G -> _S1 == _S2
5	3, 4	eleqd	_G -> (n - 1 e. _S1 <-> n - 1 e. _S2)
6	1, 2, 5	ifpeqd	_G -> (ifp (n = 0) _z1 (n - 1 e. _S1) <-> ifp (n = 0) _z2 (n - 1 e. _S2))
7	6	abeqd	_G -> {n \| ifp (n = 0) _z1 (n - 1 e. _S1)} == {n \| ifp (n = 0) _z2 (n - 1 e. _S2)}
8	7	conv ocasep	_G -> ocasep _z1 _S1 == ocasep _z2 _S2

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)