Theorem opelvvg

Description: Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015)

	Ref	Expression
Assertion	opelvvg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
3		opelxpi	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )