Metamath Proof Explorer

Theorem opabbrfexd

Description: A collection of ordered pairs, the second component being a function, is a set. (Contributed 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 opabbrfexd ⊢ φ → 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 pm4.24 ⊢ x R y ↔ x R y ∧ x R y
7 6 opabbii ⊢ x y | x R y = x y | x R y ∧ x R y
8 1 2 3 4 5 opabresexd ⊢ φ → x y | x R y ∧ x R y ∈ V
9 7 8 eqeltrid ⊢ φ → x y | x R y ∈ V