Theorem opelopabbv

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

	Ref	Expression
Hypotheses	opelopabbv.def	⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
	opelopabbv.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	opelopabbv	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opelopabbv.def	⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
2		opelopabbv.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
3	1	eleq2d	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
4		ax-5	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
5		ax-5	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
6		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
7		nfvd	⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
8	4 5 6 7 2	opelopabb	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )
9	3 8	bitrd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )