Metamath Proof Explorer

Theorem 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		unab	$⊢ \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\} \cup \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\} = \{z \| (\exists x \exists y (z = ⟨x, y⟩ \land φ) \lor \exists x \exists y (z = ⟨x, y⟩ \land ψ))\}$
2		19.43	$⊢ \exists x (\exists y (z = ⟨x, y⟩ \land φ) \lor \exists y (z = ⟨x, y⟩ \land ψ)) \leftrightarrow (\exists x \exists y (z = ⟨x, y⟩ \land φ) \lor \exists x \exists y (z = ⟨x, y⟩ \land ψ))$
3		andi	$⊢ (z = ⟨x, y⟩ \land (φ \lor ψ)) \leftrightarrow ((z = ⟨x, y⟩ \land φ) \lor (z = ⟨x, y⟩ \land ψ))$
4	3	exbii	$⊢ \exists y (z = ⟨x, y⟩ \land (φ \lor ψ)) \leftrightarrow \exists y ((z = ⟨x, y⟩ \land φ) \lor (z = ⟨x, y⟩ \land ψ))$
5		19.43	$⊢ \exists y ((z = ⟨x, y⟩ \land φ) \lor (z = ⟨x, y⟩ \land ψ)) \leftrightarrow (\exists y (z = ⟨x, y⟩ \land φ) \lor \exists y (z = ⟨x, y⟩ \land ψ))$
6	4 5	bitr2i	$⊢ (\exists y (z = ⟨x, y⟩ \land φ) \lor \exists y (z = ⟨x, y⟩ \land ψ)) \leftrightarrow \exists y (z = ⟨x, y⟩ \land (φ \lor ψ))$
7	6	exbii	$⊢ \exists x (\exists y (z = ⟨x, y⟩ \land φ) \lor \exists y (z = ⟨x, y⟩ \land ψ)) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (φ \lor ψ))$
8	2 7	bitr3i	$⊢ (\exists x \exists y (z = ⟨x, y⟩ \land φ) \lor \exists x \exists y (z = ⟨x, y⟩ \land ψ)) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (φ \lor ψ))$
9	8	abbii	$⊢ \{z \| (\exists x \exists y (z = ⟨x, y⟩ \land φ) \lor \exists x \exists y (z = ⟨x, y⟩ \land ψ))\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (φ \lor ψ))\}$
10	1 9	eqtri	$⊢ \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\} \cup \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (φ \lor ψ))\}$
11		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\}$
12		df-opab	$⊢ \{⟨x, y⟩ \| ψ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\}$
13	11 12	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 ψ)\}$
14		df-opab	$⊢ \{⟨x, y⟩ \| (φ \lor ψ)\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (φ \lor ψ))\}$
15	10 13 14	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} \cup \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| (φ \lor ψ)\}$