Theorem iunopeqop

Description: Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020) Remove antecedent. (Revised by Eric Schmidt, 9-May-2026) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	iunopeqop.b	$$⊢B\in \mathrm{V}$$
	iunopeqop.c	$$⊢C\in \mathrm{V}$$
	iunopeqop.d	$$⊢D\in \mathrm{V}$$
Assertion	iunopeqop	$$⊢\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}$$

Proof

Step	Hyp	Ref	Expression
1		iunopeqop.b	$$⊢B\in \mathrm{V}$$
2		iunopeqop.c	$$⊢C\in \mathrm{V}$$
3		iunopeqop.d	$$⊢D\in \mathrm{V}$$
4	2 3	opnzi	$$⊢⟨C,D⟩\ne \varnothing$$
5	4	a1i	$$⊢A=\varnothing \to ⟨C,D⟩\ne \varnothing$$
6		iuneq1	$$⊢A=\varnothing \to \bigcup _{x\in A}\left\{⟨x,B⟩\right\}=\bigcup _{x\in \varnothing }\left\{⟨x,B⟩\right\}$$
7		0iun	$$⊢\bigcup _{x\in \varnothing }\left\{⟨x,B⟩\right\}=\varnothing$$
8	6 7	eqtrdi	$$⊢A=\varnothing \to \bigcup _{x\in A}\left\{⟨x,B⟩\right\}=\varnothing$$
9	5 8	neeqtrrd	$$⊢A=\varnothing \to ⟨C,D⟩\ne \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
10		nesym	$$⊢⟨C,D⟩\ne \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\leftrightarrow \neg \bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩$$
11	9 10	sylib	$$⊢A=\varnothing \to \neg \bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩$$
12	11	pm2.21d	$$⊢A=\varnothing \to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
13		n0snor2el	$$⊢A\ne \varnothing \to \left(\exists x\in A\exists y\in Ax\ne y\vee \exists zA=\left\{z\right\}\right)$$
14		nfiu1	$$⊢\underset{\_}{Ⅎ}x\bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
15	14	nfeq1	$$⊢Ⅎx\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩$$
16		nfv	$$⊢Ⅎx\exists zA=\left\{z\right\}$$
17	15 16	nfim	$$⊢Ⅎx\left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
18		ssiun2	$$⊢x\in A\to \left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
20		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
21	19 20	nfop	$$⊢\underset{\_}{Ⅎ}x⟨y,⦋y/x⦌B⟩$$
22	21	nfsn	$$⊢\underset{\_}{Ⅎ}x\left\{⟨y,⦋y/x⦌B⟩\right\}$$
23	22 14	nfss	$$⊢Ⅎx\left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
24		id	$$⊢x=y\to x=y$$
25		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
26	24 25	opeq12d	$$⊢x=y\to ⟨x,B⟩=⟨y,⦋y/x⦌B⟩$$
27	26	sneqd	$$⊢x=y\to \left\{⟨x,B⟩\right\}=\left\{⟨y,⦋y/x⦌B⟩\right\}$$
28	27	sseq1d	$$⊢x=y\to \left(\left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\leftrightarrow \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\right)$$
29	19 23 28 18	vtoclgaf	$$⊢y\in A\to \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
30	18 29	anim12i	$$⊢\left(x\in A\wedge y\in A\right)\to \left(\left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\wedge \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\right)$$
31		unss	$$⊢\left(\left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\wedge \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\right)\leftrightarrow \left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
32		sseq2	$$⊢\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \left(\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\leftrightarrow \left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\right)$$
33		df-pr	$$⊢\left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}=\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}$$
34	33	eqcomi	$$⊢\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}=\left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}$$
35	34	sseq1i	$$⊢\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\leftrightarrow \left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩$$
36		vex	$$⊢x\in \mathrm{V}$$
37		vex	$$⊢y\in \mathrm{V}$$
38	1	csbex	$$⊢⦋y/x⦌B\in \mathrm{V}$$
39	36 1 37 38 2 3	propssopi	$$⊢\left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\to x=y$$
40		eqneqall	$$⊢x=y\to \left(x\ne y\to \left(\left(x\in A\wedge y\in A\right)\to \exists zA=\left\{z\right\}\right)\right)$$
41	39 40	syl	$$⊢\left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\to \left(x\ne y\to \left(\left(x\in A\wedge y\in A\right)\to \exists zA=\left\{z\right\}\right)\right)$$
42	35 41	sylbi	$$⊢\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\to \left(x\ne y\to \left(\left(x\in A\wedge y\in A\right)\to \exists zA=\left\{z\right\}\right)\right)$$
43	32 42	biimtrdi	$$⊢\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \left(\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\to \left(x\ne y\to \left(\left(x\in A\wedge y\in A\right)\to \exists zA=\left\{z\right\}\right)\right)\right)$$
44	43	com14	$$⊢\left(x\in A\wedge y\in A\right)\to \left(\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\to \left(x\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)\right)\right)$$
45	31 44	biimtrid	$$⊢\left(x\in A\wedge y\in A\right)\to \left(\left(\left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\wedge \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\right)\to \left(x\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)\right)\right)$$
46	30 45	mpd	$$⊢\left(x\in A\wedge y\in A\right)\to \left(x\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)\right)$$
47	46	rexlimdva	$$⊢x\in A\to \left(\exists y\in Ax\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)\right)$$
48	17 47	rexlimi	$$⊢\exists x\in A\exists y\in Ax\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
49		ax-1	$$⊢\exists zA=\left\{z\right\}\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
50	48 49	jaoi	$$⊢\left(\exists x\in A\exists y\in Ax\ne y\vee \exists zA=\left\{z\right\}\right)\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
51	13 50	syl	$$⊢A\ne \varnothing \to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
52	12 51	pm2.61ine	$$⊢\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}$$