Theorem rlamfunc ≪ | index | src | ≫ 

theorem rlamfunc (B: set) (a: nat) {x: nat} (b: nat x):
  $ func (\. x e. a, b) a B <-> A. x (x e. a -> b e. B) $;
StepHypRefExpression
1 bitr 
(func (\. x e. a, b) a B <-> Ran (\. x e. a, b) C_ B) ->
  (Ran (\. x e. a, b) C_ B <-> A. x (x e. a -> b e. B)) ->
  (func (\. x e. a, b) a B <-> A. x (x e. a -> b e. B))
2 bian1 
isfun (\. x e. a, b) /\ Dom (\. x e. a, b) == a -> (isfun (\. x e. a, b) /\ Dom (\. x e. a, b) == a /\ Ran (\. x e. a, b) C_ B <-> Ran (\. x e. a, b) C_ B)
3 2 conv func 
isfun (\. x e. a, b) /\ Dom (\. x e. a, b) == a -> (func (\. x e. a, b) a B <-> Ran (\. x e. a, b) C_ B)
4 ian 
isfun (\. x e. a, b) -> Dom (\. x e. a, b) == a -> isfun (\. x e. a, b) /\ Dom (\. x e. a, b) == a
5 rlamisf 
isfun (\. x e. a, b)
6 4, 5 ax_mp 
Dom (\. x e. a, b) == a -> isfun (\. x e. a, b) /\ Dom (\. x e. a, b) == a
7 dmrlam 
Dom (\. x e. a, b) == a
8 6, 7 ax_mp 
isfun (\. x e. a, b) /\ Dom (\. x e. a, b) == a
9 3, 8 ax_mp 
func (\. x e. a, b) a B <-> Ran (\. x e. a, b) C_ B
10 1, 9 ax_mp 
(Ran (\. x e. a, b) C_ B <-> A. x (x e. a -> b e. B)) -> (func (\. x e. a, b) a B <-> A. x (x e. a -> b e. B))
11 rlamrnss 
Ran (\. x e. a, b) C_ B <-> A. x (x e. a -> b e. B)
12 10, 11 ax_mp 
func (\. x e. a, b) a B <-> A. x (x e. a -> b e. B)

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), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)