Description: Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | oprabbi | ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜓 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqoprab2b | ⊢ ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ) | |
2 | 1 | biimpri | ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜓 } ) |