Theorem elopaba

Description: Membership in an ordered-pair class abstraction. (Contributed by NM, 25-Feb-2014) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	copsex2ga.1	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	elopaba	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ( 𝐴 ∈ ( V × V ) ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		copsex2ga.1	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2		elopab	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
3	1	copsex2gb	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ 𝜑 ) )
4	2 3	bitri	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ( 𝐴 ∈ ( V × V ) ∧ 𝜑 ) )