unopab

Description: Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002)

		Ref	Expression
	Assertion	unopab	$⊢ \{⟨x, y⟩ \| φ\} \cup \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| (φ \lor ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ z = w \to (z = ⟨x, y⟩ \leftrightarrow w = ⟨x, y⟩)$
2	1	anbi1d	$⊢ z = w \to ((z = ⟨x, y⟩ \land φ) \leftrightarrow (w = ⟨x, y⟩ \land φ))$
3	2	2exbidv	$⊢ z = w \to (\exists x \exists y (z = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land φ))$
4	1	anbi1d	$⊢ z = w \to ((z = ⟨x, y⟩ \land ψ) \leftrightarrow (w = ⟨x, y⟩ \land ψ))$
5	4	2exbidv	$⊢ z = w \to (\exists x \exists y (z = ⟨x, y⟩ \land ψ) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land ψ))$
6	3 5	unabw	$⊢ \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\} \cup \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\} = \{w \| (\exists x \exists y (w = ⟨x, y⟩ \land φ) \lor \exists x \exists y (w = ⟨x, y⟩ \land ψ))\}$
7		19.43	$⊢ \exists x (\exists y (w = ⟨x, y⟩ \land φ) \lor \exists y (w = ⟨x, y⟩ \land ψ)) \leftrightarrow (\exists x \exists y (w = ⟨x, y⟩ \land φ) \lor \exists x \exists y (w = ⟨x, y⟩ \land ψ))$
8		andi	$⊢ (w = ⟨x, y⟩ \land (φ \lor ψ)) \leftrightarrow ((w = ⟨x, y⟩ \land φ) \lor (w = ⟨x, y⟩ \land ψ))$
9	8	exbii	$⊢ \exists y (w = ⟨x, y⟩ \land (φ \lor ψ)) \leftrightarrow \exists y ((w = ⟨x, y⟩ \land φ) \lor (w = ⟨x, y⟩ \land ψ))$
10		19.43	$⊢ \exists y ((w = ⟨x, y⟩ \land φ) \lor (w = ⟨x, y⟩ \land ψ)) \leftrightarrow (\exists y (w = ⟨x, y⟩ \land φ) \lor \exists y (w = ⟨x, y⟩ \land ψ))$
11	9 10	bitr2i	$⊢ (\exists y (w = ⟨x, y⟩ \land φ) \lor \exists y (w = ⟨x, y⟩ \land ψ)) \leftrightarrow \exists y (w = ⟨x, y⟩ \land (φ \lor ψ))$
12	11	exbii	$⊢ \exists x (\exists y (w = ⟨x, y⟩ \land φ) \lor \exists y (w = ⟨x, y⟩ \land ψ)) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land (φ \lor ψ))$
13	7 12	bitr3i	$⊢ (\exists x \exists y (w = ⟨x, y⟩ \land φ) \lor \exists x \exists y (w = ⟨x, y⟩ \land ψ)) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land (φ \lor ψ))$
14	13	abbii	$⊢ \{w \| (\exists x \exists y (w = ⟨x, y⟩ \land φ) \lor \exists x \exists y (w = ⟨x, y⟩ \land ψ))\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land (φ \lor ψ))\}$
15	6 14	eqtri	$⊢ \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\} \cup \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land (φ \lor ψ))\}$
16		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\}$
17		df-opab	$⊢ \{⟨x, y⟩ \| ψ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\}$
18	16 17	uneq12i	$⊢ \{⟨x, y⟩ \| φ\} \cup \{⟨x, y⟩ \| ψ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\} \cup \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\}$
19		df-opab	$⊢ \{⟨x, y⟩ \| (φ \lor ψ)\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land (φ \lor ψ))\}$
20	15 18 19	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} \cup \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| (φ \lor ψ)\}$

Metamath Proof Explorer

Theorem unopab

Proof