Theorem isfeqd ≪ | index | src | ≫ 

theorem isfeqd (_G: wff) (_A1 _A2: set):
  $ _G -> _A1 == _A2 $ >
  $ _G -> (isfun _A1 <-> isfun _A2) $;
StepHypRefExpression
1 eqidd 
_G -> a, b = a, b
2 hyp _Ah 
_G -> _A1 == _A2
3 1, 2 eleqd 
_G -> (a, b e. _A1 <-> a, b e. _A2)
4 eqidd 
_G -> a, b2 = a, b2
5 4, 2 eleqd 
_G -> (a, b2 e. _A1 <-> a, b2 e. _A2)
6 biidd 
_G -> (b = b2 <-> b = b2)
7 5, 6 imeqd 
_G -> (a, b2 e. _A1 -> b = b2 <-> a, b2 e. _A2 -> b = b2)
8 3, 7 imeqd 
_G -> (a, b e. _A1 -> a, b2 e. _A1 -> b = b2 <-> a, b e. _A2 -> a, b2 e. _A2 -> b = b2)
9 8 aleqd 
_G -> (A. b2 (a, b e. _A1 -> a, b2 e. _A1 -> b = b2) <-> A. b2 (a, b e. _A2 -> a, b2 e. _A2 -> b = b2))
10 9 aleqd 
_G -> (A. b A. b2 (a, b e. _A1 -> a, b2 e. _A1 -> b = b2) <-> A. b A. b2 (a, b e. _A2 -> a, b2 e. _A2 -> b = b2))
11 10 aleqd 
_G -> (A. a A. b A. b2 (a, b e. _A1 -> a, b2 e. _A1 -> b = b2) <-> A. a A. b A. b2 (a, b e. _A2 -> a, b2 e. _A2 -> b = b2))
12 11 conv isfun 
_G -> (isfun _A1 <-> isfun _A2)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_12), axs_set (ax_8)