Theorem cbvlamh | index | src |

theorem cbvlamh {x y: nat} (a b: nat x y):
  $ FN/ y a $ >
  $ FN/ x b $ >
  $ x = y -> a = b $ >
  $ \ x, a == \ y, b $;
StepHypRefExpression
1 nfnv
FN/ y x
2 hyp h1
FN/ y a
3 1, 2 nfpr
FN/ y x, a
4 3 nfeq2
F/ y p1 = x, a
5 nfnv
FN/ x y
6 hyp h2
FN/ x b
7 5, 6 nfpr
FN/ x y, b
8 7 nfeq2
F/ x p1 = y, b
9 id
x = y -> x = y
10 hyp e
x = y -> a = b
11 9, 10 preqd
x = y -> x, a = y, b
12 11 eqeq2d
x = y -> (p1 = x, a <-> p1 = y, b)
13 4, 8, 12 cbvexh
E. x p1 = x, a <-> E. y p1 = y, b
14 eqeq1
p1 = p2 -> (p1 = y, b <-> p2 = y, b)
15 14 exeqd
p1 = p2 -> (E. y p1 = y, b <-> E. y p2 = y, b)
16 13, 15 syl5bb
p1 = p2 -> (E. x p1 = x, a <-> E. y p2 = y, b)
17 16 cbvab
{p1 | E. x p1 = x, a} == {p2 | E. y p2 = y, b}
18 17 conv lam
\ x, a == \ y, 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 (peano2, addeq, muleq)