Theorem subsnsn2 | index | src |

theorem subsnsn2 (a: nat) {x: nat}: $ subsn {x | x = a} $;
StepHypRefExpression
1 eqeq1
x = u -> (x = a <-> u = a)
2 1 elabe
u e. {x | x = a} <-> u = a
3 anl
u e. {x | x = a} /\ v e. {x | x = a} -> u e. {x | x = a}
4 2, 3 sylib
u e. {x | x = a} /\ v e. {x | x = a} -> u = a
5 eqeq1
x = v -> (x = a <-> v = a)
6 5 elabe
v e. {x | x = a} <-> v = a
7 anr
u e. {x | x = a} /\ v e. {x | x = a} -> v e. {x | x = a}
8 6, 7 sylib
u e. {x | x = a} /\ v e. {x | x = a} -> v = a
9 4, 8 eqtr4d
u e. {x | x = a} /\ v e. {x | x = a} -> u = v
10 9 exp
u e. {x | x = a} -> v e. {x | x = a} -> u = v
11 10 ax_gen
A. v (u e. {x | x = a} -> v e. {x | x = a} -> u = v)
12 11 ax_gen
A. u A. v (u e. {x | x = a} -> v e. {x | x = a} -> u = v)
13 12 conv subsn
subsn {x | x = a}

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)