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 | ||
opabresex0d.t | |||
opabresex0d.y | |||
opabresex0d.c | |||
Assertion | opabbrfex0d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opabresex0d.x | ||
2 | opabresex0d.t | ||
3 | opabresex0d.y | ||
4 | opabresex0d.c | ||
5 | pm4.24 | ||
6 | 5 | opabbii | |
7 | 1 2 3 4 | opabresex0d | |
8 | 6 7 | eqeltrid |