Description: A set is an element of the domain of a ordered pair class abstraction iff there is a second set so that both sets fulfil the wff of the class abstraction. (Contributed by AV, 19-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dmopabel.d | ⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ 𝜓 ) ) | |
Assertion | dmopabelb | ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ dom { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑦 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmopabel.d | ⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ 𝜓 ) ) | |
2 | dmopab | ⊢ dom { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = { 𝑥 ∣ ∃ 𝑦 𝜑 } | |
3 | 2 | eleq2i | ⊢ ( 𝑋 ∈ dom { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑦 𝜑 } ) |
4 | 1 | exbidv | ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜓 ) ) |
5 | eqid | ⊢ { 𝑥 ∣ ∃ 𝑦 𝜑 } = { 𝑥 ∣ ∃ 𝑦 𝜑 } | |
6 | 4 5 | elab2g | ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑦 𝜑 } ↔ ∃ 𝑦 𝜓 ) ) |
7 | 3 6 | syl5bb | ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ dom { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑦 𝜓 ) ) |