Theorem elvv

Description: Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994) (Proof shortened by BJ, 16-Oct-2026)

	Ref	Expression
Assertion	elvv	⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		elxp2	⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∈ V ∃ 𝑦 ∈ V 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2		rexv	⊢ ( ∃ 𝑥 ∈ V ∃ 𝑦 ∈ V 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ∈ V 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
3		rexv	⊢ ( ∃ 𝑦 ∈ V 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
4	3	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ V 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
5	1 2 4	3bitri	⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )