Theorem wl-exeq

Description: The semantics of E. x y = z . (Contributed by Wolf Lammen, 27-Apr-2018)

	Ref	Expression
Assertion	wl-exeq	$$⊢\exists xy=z\leftrightarrow \left(y=z\vee \forall xx=y\vee \forall xx=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfeqf	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxy=z$$
2	1	19.9d	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\exists xy=z\to y=z\right)$$
3	2	impancom	$$⊢\left(\neg \forall xx=y\wedge \exists xy=z\right)\to \left(\neg \forall xx=z\to y=z\right)$$
4	3	orrd	$$⊢\left(\neg \forall xx=y\wedge \exists xy=z\right)\to \left(\forall xx=z\vee y=z\right)$$
5	4	expcom	$$⊢\exists xy=z\to \left(\neg \forall xx=y\to \left(\forall xx=z\vee y=z\right)\right)$$
6	5	orrd	$$⊢\exists xy=z\to \left(\forall xx=y\vee \left(\forall xx=z\vee y=z\right)\right)$$
7		3orass	$$⊢\left(\forall xx=y\vee \forall xx=z\vee y=z\right)\leftrightarrow \left(\forall xx=y\vee \left(\forall xx=z\vee y=z\right)\right)$$
8	6 7	sylibr	$$⊢\exists xy=z\to \left(\forall xx=y\vee \forall xx=z\vee y=z\right)$$
9		3orrot	$$⊢\left(y=z\vee \forall xx=y\vee \forall xx=z\right)\leftrightarrow \left(\forall xx=y\vee \forall xx=z\vee y=z\right)$$
10	8 9	sylibr	$$⊢\exists xy=z\to \left(y=z\vee \forall xx=y\vee \forall xx=z\right)$$
11		19.8a	$$⊢y=z\to \exists xy=z$$
12		ax6e	$$⊢\exists xx=z$$
13		ax7	$$⊢x=y\to \left(x=z\to y=z\right)$$
14	13	com12	$$⊢x=z\to \left(x=y\to y=z\right)$$
15	12 14	eximii	$$⊢\exists x\left(x=y\to y=z\right)$$
16	15	19.35i	$$⊢\forall xx=y\to \exists xy=z$$
17		ax6e	$$⊢\exists xx=y$$
18	17 13	eximii	$$⊢\exists x\left(x=z\to y=z\right)$$
19	18	19.35i	$$⊢\forall xx=z\to \exists xy=z$$
20	11 16 19	3jaoi	$$⊢\left(y=z\vee \forall xx=y\vee \forall xx=z\right)\to \exists xy=z$$
21	10 20	impbii	$$⊢\exists xy=z\leftrightarrow \left(y=z\vee \forall xx=y\vee \forall xx=z\right)$$