Metamath Proof Explorer

Theorem opabresex0d

Description: A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 1-Jan-2021)

Ref Expression
Hypotheses opabresex0d.x ⊢ φ ∧ x R y → x ∈ C
opabresex0d.t ⊢ φ ∧ x R y → θ
opabresex0d.y ⊢ φ ∧ x ∈ C → y | θ ∈ V
opabresex0d.c ⊢ φ → C ∈ W
Assertion opabresex0d ⊢ φ → x y | x R y ∧ ψ ∈ V

Proof

Step Hyp Ref Expression
1 opabresex0d.x ⊢ φ ∧ x R y → x ∈ C
2 opabresex0d.t ⊢ φ ∧ x R y → θ
3 opabresex0d.y ⊢ φ ∧ x ∈ C → y | θ ∈ V
4 opabresex0d.c ⊢ φ → C ∈ W
5 1 2 jca ⊢ φ ∧ x R y → x ∈ C ∧ θ
6 5 ex ⊢ φ → x R y → x ∈ C ∧ θ
7 6 alrimivv ⊢ φ → ∀ x ∀ y x R y → x ∈ C ∧ θ
8 3 elexd ⊢ φ ∧ x ∈ C → y | θ ∈ V
9 4 8 opabex3d ⊢ φ → x y | x ∈ C ∧ θ ∈ V
10 opabbrex ⊢ ∀ x ∀ y x R y → x ∈ C ∧ θ ∧ x y | x ∈ C ∧ θ ∈ V → x y | x R y ∧ ψ ∈ V
11 7 9 10 syl2anc ⊢ φ → x y | x R y ∧ ψ ∈ V