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	⊢ ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ → ¬ ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
2		opprc	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
3	1 2	nsyl2	⊢ ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )