Theorem elwrite | index | src |

theorem elwrite (F: set) (a b x y: nat):
  $ x, y e. write F a b <-> ifp (x = a) (y = b) (x, y e. F) $;
StepHypRefExpression
1 anl
a1 = x /\ a2 = y -> a1 = x
2 1 eqeq1d
a1 = x /\ a2 = y -> (a1 = a <-> x = a)
3 anr
a1 = x /\ a2 = y -> a2 = y
4 3 eqeq1d
a1 = x /\ a2 = y -> (a2 = b <-> y = b)
5 preq
a1 = x -> a2 = y -> a1, a2 = x, y
6 5 imp
a1 = x /\ a2 = y -> a1, a2 = x, y
7 6 eleq1d
a1 = x /\ a2 = y -> (a1, a2 e. F <-> x, y e. F)
8 2, 4, 7 ifpeqd
a1 = x /\ a2 = y -> (ifp (a1 = a) (a2 = b) (a1, a2 e. F) <-> ifp (x = a) (y = b) (x, y e. F))
9 8 elabed
a1 = x -> (y e. {a2 | ifp (a1 = a) (a2 = b) (a1, a2 e. F)} <-> ifp (x = a) (y = b) (x, y e. F))
10 9 elsabe
x, y e. S\ a1, {a2 | ifp (a1 = a) (a2 = b) (a1, a2 e. F)} <-> ifp (x = a) (y = b) (x, y e. F)
11 10 conv write
x, y e. write F a b <-> ifp (x = a) (y = b) (x, y e. F)

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)