Theorem rlamfunc2 ≪ | index | src | ≫ 

theorem rlamfunc2 (A B: set) (a: nat) {x: nat} (b: nat x):
  $ A == a -> (func (\. x e. a, b) A B <-> A. x (x e. A -> b e. B)) $;
StepHypRefExpression
1 rlamfunc 
func (\. x e. a, b) a B <-> A. x (x e. a -> b e. B)
2 eqsidd 
A == a -> \. x e. a, b == \. x e. a, b
3 id 
A == a -> A == a
4 eqsidd 
A == a -> B == B
5 2, 3, 4 funceqd 
A == a -> (func (\. x e. a, b) A B <-> func (\. x e. a, b) a B)
6 eqidd 
A == a -> x = x
7 6, 3 eleqd 
A == a -> (x e. A <-> x e. a)
8 biidd 
A == a -> (b e. B <-> b e. B)
9 7, 8 imeqd 
A == a -> (x e. A -> b e. B <-> x e. a -> b e. B)
10 9 aleqd 
A == a -> (A. x (x e. A -> b e. B) <-> A. x (x e. a -> b e. B))
11 5, 10 bieqd 
A == a -> (func (\. x e. a, b) A B <-> A. x (x e. A -> b e. B) <-> (func (\. x e. a, b) a B <-> A. x (x e. a -> b e. B)))
12 1, 11 mpbiri 
A == a -> (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)