Given ¬A we have (if A then x else y) = y.
Proof
let M = {u | A ∧ u = x ∨ ¬A ∧ u = y}.
01. 1 ⊢ set y, hypo.
02. 2 ⊢ ¬A, hypo.
03. 3 ⊢ u ∈ M, hypo.
04. 3 ⊢ A ∧ u = x ∨ ¬A ∧ u = y, comp_elim 3.
05. 5 ⊢ A ∧ u = x, hypo.
06. 5 ⊢ A, conj_eliml 5.
07. 2, 5 ⊢ ⊥, neg_elim 2 6.
08. 2, 5 ⊢ u = y, efq 7.
09. 9 ⊢ ¬A ∧ u = y, hypo.
10. 9 ⊢ u = y, conj_elimr 9.
11. 2, 3 ⊢ u = y, disj_elim 4 8 10.
12. 1, 2, 3 ⊢ u ∈ {y}, sg_intro 1 11.
13. 1, 2 ⊢ u ∈ M → u ∈ {y}, subj_intro 12.
14. 14 ⊢ u ∈ {y}, hypo.
15. 1, 14 ⊢ u = y, sg_elim 1 14.
16. 1, 2, 14 ⊢ ¬A ∧ u = y, conj_intro 2 15.
17. 1, 2, 14 ⊢ A ∧ u = x ∨ ¬A ∧ u = y, disj_intror 16.
18. 14 ⊢ set u, set_intro 14.
19. 1, 2, 14 ⊢ u ∈ M, comp_intro 18 17.
20. 1, 2 ⊢ u ∈ {y} → u ∈ M, subj_intro 19.
21. 1, 2 ⊢ u ∈ M ↔ u ∈ {y}, bij_intro 13 20.
22. 1, 2 ⊢ ∀u. u ∈ M ↔ u ∈ {y}, uq_intro 21.
23. 1, 2 ⊢ M = {y}, ext 22.
24. 1, 2 ⊢ ⋂M = ⋂{y}, eq_cong 23, f t = ⋂t.
25. 1 ⊢ ⋂{y} = y, Intersection_sg 1.
26. 1, 2 ⊢ ⋂M = y, eq_trans 24 25.
27. 1, 2 ⊢ if A x y = y, eq_trans cond_eq 26.
cond_eqr. ⊢ set y → ¬A → if A x y = y, subj_intro_ii 27.
Dependencies
The given proof depends on five axioms:
comp, efq, eq_refl, eq_subst, ext.