Theorem elopab

Description: Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998)

	Ref	Expression
Assertion	elopab	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → 𝐴 ∈ V )
2		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
3		eleq1	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ V ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ V ) )
4	2 3	mpbiri	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 ∈ V )
5	4	adantr	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝐴 ∈ V )
6	5	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝐴 ∈ V )
7		elopabw	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
8	1 6 7	pm5.21nii	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )