Metamath Proof Explorer


Theorem opabbrfex0d

Description: A collection of ordered pairs, the class of all possible second components being a set, is a set. (Contributed by AV, 15-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 opabbrfex0d φ 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 pm4.24 x R y x R y x R y
6 5 opabbii x y | x R y = x y | x R y x R y
7 1 2 3 4 opabresex0d φ x y | x R y x R y V
8 6 7 eqeltrid φ x y | x R y V