Theorem unrlam ≪ | index | src | ≫ 

theorem unrlam (a b c: nat) {x: nat} (v: nat x):
  $ (\. x e. a, v) u. (\. x e. b, v) == \. x e. c, v <-> a u. b == c $;
StepHypRefExpression
1 eqstr 
Dom ((\. x e. a, v) u. (\. x e. b, v)) == Dom (\. x e. a, v) u. Dom (\. x e. b, v) ->
  Dom (\. x e. a, v) u. Dom (\. x e. b, v) == a u. b ->
  Dom ((\. x e. a, v) u. (\. x e. b, v)) == a u. b
2 dmun 
Dom ((\. x e. a, v) u. (\. x e. b, v)) == Dom (\. x e. a, v) u. Dom (\. x e. b, v)
3 1, 2 ax_mp 
Dom (\. x e. a, v) u. Dom (\. x e. b, v) == a u. b -> Dom ((\. x e. a, v) u. (\. x e. b, v)) == a u. b
4 uneq 
Dom (\. x e. a, v) == a -> Dom (\. x e. b, v) == b -> Dom (\. x e. a, v) u. Dom (\. x e. b, v) == a u. b
5 dmrlam 
Dom (\. x e. a, v) == a
6 4, 5 ax_mp 
Dom (\. x e. b, v) == b -> Dom (\. x e. a, v) u. Dom (\. x e. b, v) == a u. b
7 dmrlam 
Dom (\. x e. b, v) == b
8 6, 7 ax_mp 
Dom (\. x e. a, v) u. Dom (\. x e. b, v) == a u. b
9 3, 8 ax_mp 
Dom ((\. x e. a, v) u. (\. x e. b, v)) == a u. b
10 dmrlam 
Dom (\. x e. c, v) == c
11 dmeq 
(\. x e. a, v) u. (\. x e. b, v) == \. x e. c, v -> Dom ((\. x e. a, v) u. (\. x e. b, v)) == Dom (\. x e. c, v)
12 9, 10, 11 eqstr3g 
(\. x e. a, v) u. (\. x e. b, v) == \. x e. c, v -> a u. b == c
13 bitr 
(a1 e. (\. x e. a, v) u. (\. x e. b, v) <-> a1 e. \. x e. a, v \/ a1 e. \. x e. b, v) ->
  (a1 e. \. x e. a, v \/ a1 e. \. x e. b, v <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v)) ->
  (a1 e. (\. x e. a, v) u. (\. x e. b, v) <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v))
14 elun 
a1 e. (\. x e. a, v) u. (\. x e. b, v) <-> a1 e. \. x e. a, v \/ a1 e. \. x e. b, v
15 13, 14 ax_mp 
(a1 e. \. x e. a, v \/ a1 e. \. x e. b, v <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v)) ->
  (a1 e. (\. x e. a, v) u. (\. x e. b, v) <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v))
16 oreq 
(a1 e. \. x e. a, v <-> E. x (x e. a /\ a1 = x, v)) ->
  (a1 e. \. x e. b, v <-> E. x (x e. b /\ a1 = x, v)) ->
  (a1 e. \. x e. a, v \/ a1 e. \. x e. b, v <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v))
17 elrlam 
a1 e. \. x e. a, v <-> E. x (x e. a /\ a1 = x, v)
18 16, 17 ax_mp 
(a1 e. \. x e. b, v <-> E. x (x e. b /\ a1 = x, v)) -> (a1 e. \. x e. a, v \/ a1 e. \. x e. b, v <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v))
19 elrlam 
a1 e. \. x e. b, v <-> E. x (x e. b /\ a1 = x, v)
20 18, 19 ax_mp 
a1 e. \. x e. a, v \/ a1 e. \. x e. b, v <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v)
21 15, 20 ax_mp 
a1 e. (\. x e. a, v) u. (\. x e. b, v) <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v)
22 elrlam 
a1 e. \. x e. c, v <-> E. x (x e. c /\ a1 = x, v)
23 exor 
E. x (x e. a /\ a1 = x, v \/ x e. b /\ a1 = x, v) <-> E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v)
24 andir 
(x e. a \/ x e. b) /\ a1 = x, v <-> x e. a /\ a1 = x, v \/ x e. b /\ a1 = x, v
25 elun 
x e. a u. b <-> x e. a \/ x e. b
26 eleq2 
a u. b == c -> (x e. a u. b <-> x e. c)
27 25, 26 syl5bbr 
a u. b == c -> (x e. a \/ x e. b <-> x e. c)
28 27 aneq1d 
a u. b == c -> ((x e. a \/ x e. b) /\ a1 = x, v <-> x e. c /\ a1 = x, v)
29 24, 28 syl5bbr 
a u. b == c -> (x e. a /\ a1 = x, v \/ x e. b /\ a1 = x, v <-> x e. c /\ a1 = x, v)
30 29 exeqd 
a u. b == c -> (E. x (x e. a /\ a1 = x, v \/ x e. b /\ a1 = x, v) <-> E. x (x e. c /\ a1 = x, v))
31 23, 30 syl5bbr 
a u. b == c -> (E. x (x e. a /\ a1 = x, v) \/ E. x (x e. b /\ a1 = x, v) <-> E. x (x e. c /\ a1 = x, v))
32 21, 22, 31 bitr4g 
a u. b == c -> (a1 e. (\. x e. a, v) u. (\. x e. b, v) <-> a1 e. \. x e. c, v)
33 32 eqrd 
a u. b == c -> (\. x e. a, v) u. (\. x e. b, v) == \. x e. c, v
34 12, 33 ibii 
(\. x e. a, v) u. (\. x e. b, v) == \. x e. c, v <-> a u. b == c

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)