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 ) ∧ 𝜒 ) ) ) |
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 ) ∧ 𝜒 ) ) ) |