Description: Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007) (Revised by Mario Carneiro, 19-Dec-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opelopab2.1 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
opelopab2.2 | ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) | ||
Assertion | opelopab2 | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜑 ) } ↔ 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelopab2.1 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
2 | opelopab2.2 | ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) | |
3 | 1 2 | sylan9bb | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) |
4 | 3 | opelopab2a | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜑 ) } ↔ 𝜒 ) ) |