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