Description: Deduce equality of a relation and an ordered-pair class abstraction. Compare abbi2dv . (Contributed by NM, 24-Feb-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opabbi2dv.1 | ⊢ Rel 𝐴 | |
opabbi2dv.3 | ⊢ ( 𝜑 → ( 〈 𝑥 , 𝑦 〉 ∈ 𝐴 ↔ 𝜓 ) ) | ||
Assertion | opabbi2dv | ⊢ ( 𝜑 → 𝐴 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opabbi2dv.1 | ⊢ Rel 𝐴 | |
2 | opabbi2dv.3 | ⊢ ( 𝜑 → ( 〈 𝑥 , 𝑦 〉 ∈ 𝐴 ↔ 𝜓 ) ) | |
3 | opabid2 | ⊢ ( Rel 𝐴 → { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } = 𝐴 ) | |
4 | 1 3 | ax-mp | ⊢ { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } = 𝐴 |
5 | 2 | opabbidv | ⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } = { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ) |
6 | 4 5 | syl5eqr | ⊢ ( 𝜑 → 𝐴 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ) |