Theorem dmlam ≪ | index | src | ≫ 

theorem dmlam {x: nat} (a: nat x): $ Dom (\ x, a) == _V $;
StepHypRefExpression
1 bith 
y e. Dom (\ x, a) -> y e. _V -> (y e. Dom (\ x, a) <-> y e. _V)
2 preldm 
y, N[y / x] a e. \ x, a -> y e. Dom (\ x, a)
3 eleq2 
\ x, a == \ z, N[z / x] a -> (y, N[y / x] a e. \ x, a <-> y, N[y / x] a e. \ z, N[z / x] a)
4 cbvlams 
\ x, a == \ z, N[z / x] a
5 3, 4 ax_mp 
y, N[y / x] a e. \ x, a <-> y, N[y / x] a e. \ z, N[z / x] a
6 ellam 
y, N[y / x] a e. \ z, N[z / x] a <-> E. z y, N[y / x] a = z, N[z / x] a
7 id 
z = y -> z = y
8 sbneq1 
z = y -> N[z / x] a = N[y / x] a
9 7, 8 preqd 
z = y -> z, N[z / x] a = y, N[y / x] a
10 9 eqeq2d 
z = y -> (y, N[y / x] a = z, N[z / x] a <-> y, N[y / x] a = y, N[y / x] a)
11 10 iexe 
y, N[y / x] a = y, N[y / x] a -> E. z y, N[y / x] a = z, N[z / x] a
12 eqid 
y, N[y / x] a = y, N[y / x] a
13 11, 12 ax_mp 
E. z y, N[y / x] a = z, N[z / x] a
14 6, 13 mpbir 
y, N[y / x] a e. \ z, N[z / x] a
15 5, 14 mpbir 
y, N[y / x] a e. \ x, a
16 2, 15 ax_mp 
y e. Dom (\ x, a)
17 1, 16 ax_mp 
y e. _V -> (y e. Dom (\ x, a) <-> y e. _V)
18 elv 
y e. _V
19 17, 18 ax_mp 
y e. Dom (\ x, a) <-> y e. _V
20 19 eqri 
Dom (\ x, a) == _V

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)