Description: A collection of ordered pairs, the second component being a function, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 15-Jan-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | opabresexd.x | ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐶 ) | |
| opabresexd.y | ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 : 𝐴 ⟶ 𝐵 ) | ||
| opabresexd.a | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐴 ∈ 𝑈 ) | ||
| opabresexd.b | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ 𝑉 ) | ||
| opabresexd.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 ) | ||
| Assertion | opabresexd | ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) } ∈ V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opabresexd.x | ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐶 ) | |
| 2 | opabresexd.y | ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 : 𝐴 ⟶ 𝐵 ) | |
| 3 | opabresexd.a | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐴 ∈ 𝑈 ) | |
| 4 | opabresexd.b | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ 𝑉 ) | |
| 5 | opabresexd.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 ) | |
| 6 | mapex | ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) → { 𝑦 ∣ 𝑦 : 𝐴 ⟶ 𝐵 } ∈ V ) | |
| 7 | 3 4 6 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → { 𝑦 ∣ 𝑦 : 𝐴 ⟶ 𝐵 } ∈ V ) |
| 8 | 1 2 7 5 | opabresex0d | ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) } ∈ V ) |