Metamath Proof Explorer

Theorem opabresexd

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 ⊢ φ ∧ x R y → x ∈ C
opabresexd.y ⊢ φ ∧ x R y → y : A ⟶ B
opabresexd.a ⊢ φ ∧ x ∈ C → A ∈ U
opabresexd.b ⊢ φ ∧ x ∈ C → B ∈ V
opabresexd.c ⊢ φ → C ∈ W
Assertion opabresexd ⊢ φ → x y | x R y ∧ ψ ∈ V

Proof

Step Hyp Ref Expression
1 opabresexd.x ⊢ φ ∧ x R y → x ∈ C
2 opabresexd.y ⊢ φ ∧ x R y → y : A ⟶ B
3 opabresexd.a ⊢ φ ∧ x ∈ C → A ∈ U
4 opabresexd.b ⊢ φ ∧ x ∈ C → B ∈ V
5 opabresexd.c ⊢ φ → C ∈ W
6 mapex ⊢ A ∈ U ∧ B ∈ V → y | y : A ⟶ B ∈ V
7 3 4 6 syl2anc ⊢ φ ∧ x ∈ C → y | y : A ⟶ B ∈ V
8 1 2 7 5 opabresex0d ⊢ φ → x y | x R y ∧ ψ ∈ V