Description: Restrictions of a collection of ordered pairs of related elements are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 15-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opabresex2d.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ) → 𝜓 ) | |
opabresex2d.2 | ⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∈ 𝑉 ) | ||
Assertion | opabresex2d | ⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ∧ 𝜃 ) } ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opabresex2d.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ) → 𝜓 ) | |
2 | opabresex2d.2 | ⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∈ 𝑉 ) | |
3 | 1 | ex | ⊢ ( 𝜑 → ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 → 𝜓 ) ) |
4 | 3 | alrimivv | ⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 → 𝜓 ) ) |
5 | opabbrex | ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 → 𝜓 ) ∧ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∈ 𝑉 ) → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ∧ 𝜃 ) } ∈ V ) | |
6 | 4 2 5 | syl2anc | ⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ∧ 𝜃 ) } ∈ V ) |