Theorem oprcl

Description: If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	oprcl	$$⊢C\in ⟨A,B⟩\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢C\in ⟨A,B⟩\to \neg ⟨A,B⟩=\varnothing$$
2		opprc	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to ⟨A,B⟩=\varnothing$$
3	1 2	nsyl2	$$⊢C\in ⟨A,B⟩\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$