Theorem rlameq2b | index | src |

theorem rlameq2b (a: nat) {x: nat} (v w: nat x):
  $ \. x e. a, v = \. x e. a, w <-> A. x (x e. a -> v = w) $;
StepHypRefExpression
1 nfnv
FN/ x a
2 1 nfrlam1
FN/ x \. x e. a, v
3 1 nfrlam1
FN/ x \. x e. a, w
4 2, 3 nf_eq
F/ x \. x e. a, v = \. x e. a, w
5 appneq1
\. x e. a, v = \. x e. a, w -> (\. x e. a, v) @ x = (\. x e. a, w) @ x
6 apprlam
x e. a -> (\. x e. a, v) @ x = v
7 apprlam
x e. a -> (\. x e. a, w) @ x = w
8 6, 7 eqeqd
x e. a -> ((\. x e. a, v) @ x = (\. x e. a, w) @ x <-> v = w)
9 8 bi1d
x e. a -> (\. x e. a, v) @ x = (\. x e. a, w) @ x -> v = w
10 9 com12
(\. x e. a, v) @ x = (\. x e. a, w) @ x -> x e. a -> v = w
11 5, 10 rsyl
\. x e. a, v = \. x e. a, w -> x e. a -> v = w
12 4, 11 ialdh
\. x e. a, v = \. x e. a, w -> A. x (x e. a -> v = w)
13 rlameq2a
A. x (x e. a -> v = w) -> \. x e. a, v = \. x e. a, w
14 12, 13 ibii
\. x e. a, v = \. x e. a, w <-> A. x (x e. a -> v = w)

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)