Metamath Proof Explorer


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 syl5bb ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )