Theorem opelopabb

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

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

Proof

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