Theorem opelopabd

Description: Membership of an ordered pair in a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023)

	Ref	Expression
Hypotheses	opelopabd.xph	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	opelopabd.yph	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
	opelopabd.xch	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	opelopabd.ych	⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
	opelopabd.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	opelopabd.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	opelopabd.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	opelopabd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		opelopabd.xph	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		opelopabd.yph	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
3		opelopabd.xch	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
4		opelopabd.ych	⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
5		opelopabd.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
6		opelopabd.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7		opelopabd.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
8		elopab	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
9	1 2 3 4 5 6 7	copsex2d	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ 𝜒 ) )
10	8 9	bitrid	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ 𝜒 ) )