Theorem funceqd ≪ | index | src | ≫

theorem funceqd (_G: wff) (_F1 _F2 _A1 _A2 _B1 _B2: set):
  $ _G -> _F1 == _F2 $ >
  $ _G -> _A1 == _A2 $ >
  $ _G -> _B1 == _B2 $ >
  $ _G -> (func _F1 _A1 _B1 <-> func _F2 _A2 _B2) $;


_G -> _F1 == _F2
_G -> (isfun _F1 <-> isfun _F2)
_G -> Dom _F1 == Dom _F2
_G -> _A1 == _A2
_G -> (Dom _F1 == _A1 <-> Dom _F2 == _A2)
_G -> (isfun _F1 /\ Dom _F1 == _A1 <-> isfun _F2 /\ Dom _F2 == _A2)
_G -> Ran _F1 == Ran _F2
_G -> _B1 == _B2
_G -> (Ran _F1 C_ _B1 <-> Ran _F2 C_ _B2)
_G -> (isfun _F1 /\ Dom _F1 == _A1 /\ Ran _F1 C_ _B1 <-> isfun _F2 /\ Dom _F2 == _A2 /\ Ran _F2 C_ _B2)
_G -> (func _F1 _A1 _B1 <-> func _F2 _A2 _B2)

Step	Hyp	Ref	Expression
1		hyp _Fh	_G -> _F1 == _F2
2	1	isfeqd	_G -> (isfun _F1 <-> isfun _F2)
3	1	dmeqd	_G -> Dom _F1 == Dom _F2
4		hyp _Ah	_G -> _A1 == _A2
5	3, 4	eqseqd	_G -> (Dom _F1 == _A1 <-> Dom _F2 == _A2)
6	2, 5	aneqd	_G -> (isfun _F1 /\ Dom _F1 == _A1 <-> isfun _F2 /\ Dom _F2 == _A2)
7	1	rneqd	_G -> Ran _F1 == Ran _F2
8		hyp _Bh	_G -> _B1 == _B2
9	7, 8	sseqd	_G -> (Ran _F1 C_ _B1 <-> Ran _F2 C_ _B2)
10	6, 9	aneqd	_G -> (isfun _F1 /\ Dom _F1 == _A1 /\ Ran _F1 C_ _B1 <-> isfun _F2 /\ Dom _F2 == _A2 /\ Ran _F2 C_ _B2)
11	10	conv func	_G -> (func _F1 _A1 _B1 <-> func _F2 _A2 _B2)

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)