Theorem eusvobj2

Description: Specify the same property in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010) (Proof shortened by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Hypothesis	eusvobj1.1	$$⊢B\in \mathrm{V}$$
Assertion	eusvobj2	$$⊢\exists !x\exists y\in Ax=B\to \left(\exists y\in Ax=B\leftrightarrow \forall y\in Ax=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eusvobj1.1	$$⊢B\in \mathrm{V}$$
2		euabsn2	$$⊢\exists !x\exists y\in Ax=B\leftrightarrow \exists z\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}$$
3		eleq2	$$⊢\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \left(x\in \left\{x|\exists y\in Ax=B\right\}\leftrightarrow x\in \left\{z\right\}\right)$$
4		abid	$$⊢x\in \left\{x|\exists y\in Ax=B\right\}\leftrightarrow \exists y\in Ax=B$$
5		velsn	$$⊢x\in \left\{z\right\}\leftrightarrow x=z$$
6	3 4 5	3bitr3g	$$⊢\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \left(\exists y\in Ax=B\leftrightarrow x=z\right)$$
7		nfre1	$$⊢Ⅎy\exists y\in Ax=B$$
8	7	nfab	$$⊢\underset{\_}{Ⅎ}y\left\{x|\exists y\in Ax=B\right\}$$
9	8	nfeq1	$$⊢Ⅎy\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}$$
10	1	elabrex	$$⊢y\in A\to B\in \left\{x|\exists y\in Ax=B\right\}$$
11		eleq2	$$⊢\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \left(B\in \left\{x|\exists y\in Ax=B\right\}\leftrightarrow B\in \left\{z\right\}\right)$$
12	1	elsn	$$⊢B\in \left\{z\right\}\leftrightarrow B=z$$
13		eqcom	$$⊢B=z\leftrightarrow z=B$$
14	12 13	bitri	$$⊢B\in \left\{z\right\}\leftrightarrow z=B$$
15	11 14	bitrdi	$$⊢\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \left(B\in \left\{x|\exists y\in Ax=B\right\}\leftrightarrow z=B\right)$$
16	10 15	syl5ib	$$⊢\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \left(y\in A\to z=B\right)$$
17	9 16	ralrimi	$$⊢\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \forall y\in Az=B$$
18		eqeq1	$$⊢x=z\to \left(x=B\leftrightarrow z=B\right)$$
19	18	ralbidv	$$⊢x=z\to \left(\forall y\in Ax=B\leftrightarrow \forall y\in Az=B\right)$$
20	17 19	syl5ibrcom	$$⊢\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \left(x=z\to \forall y\in Ax=B\right)$$
21	6 20	sylbid	$$⊢\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \left(\exists y\in Ax=B\to \forall y\in Ax=B\right)$$
22	21	exlimiv	$$⊢\exists z\left\{x|\exists y\in Ax=B\right\}=\left\{z\right\}\to \left(\exists y\in Ax=B\to \forall y\in Ax=B\right)$$
23	2 22	sylbi	$$⊢\exists !x\exists y\in Ax=B\to \left(\exists y\in Ax=B\to \forall y\in Ax=B\right)$$
24		euex	$$⊢\exists !x\exists y\in Ax=B\to \exists x\exists y\in Ax=B$$
25		rexn0	$$⊢\exists y\in Ax=B\to A\ne \varnothing$$
26	25	exlimiv	$$⊢\exists x\exists y\in Ax=B\to A\ne \varnothing$$
27		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall y\in Ax=B\right)\to \exists y\in Ax=B$$
28	27	ex	$$⊢A\ne \varnothing \to \left(\forall y\in Ax=B\to \exists y\in Ax=B\right)$$
29	24 26 28	3syl	$$⊢\exists !x\exists y\in Ax=B\to \left(\forall y\in Ax=B\to \exists y\in Ax=B\right)$$
30	23 29	impbid	$$⊢\exists !x\exists y\in Ax=B\to \left(\exists y\in Ax=B\leftrightarrow \forall y\in Ax=B\right)$$