Theorem uniopel

Description: Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	opthw.1	$$⊢A\in \mathrm{V}$$
	opthw.2	$$⊢B\in \mathrm{V}$$
Assertion	uniopel	$$⊢⟨A,B⟩\in C\to \bigcup ⟨A,B⟩\in \bigcup C$$

Proof

Step	Hyp	Ref	Expression
1		opthw.1	$$⊢A\in \mathrm{V}$$
2		opthw.2	$$⊢B\in \mathrm{V}$$
3	1 2	uniop	$$⊢\bigcup ⟨A,B⟩=\left\{A,B\right\}$$
4	1 2	opi2	$$⊢\left\{A,B\right\}\in ⟨A,B⟩$$
5	3 4	eqeltri	$$⊢\bigcup ⟨A,B⟩\in ⟨A,B⟩$$
6		elssuni	$$⊢⟨A,B⟩\in C\to ⟨A,B⟩\subseteq \bigcup C$$
7	6	sseld	$$⊢⟨A,B⟩\in C\to \left(\bigcup ⟨A,B⟩\in ⟨A,B⟩\to \bigcup ⟨A,B⟩\in \bigcup C\right)$$
8	5 7	mpi	$$⊢⟨A,B⟩\in C\to \bigcup ⟨A,B⟩\in \bigcup C$$