Metamath Proof Explorer


Theorem opabbrex

Description: A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by BJ/AV, 20-Jun-2019) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Assertion opabbrex xyxRyφxy|φVxy|xRyψV

Proof

Step Hyp Ref Expression
1 simpr xyxRyφxy|φVxy|φV
2 pm3.41 xRyφxRyψφ
3 2 2alimi xyxRyφxyxRyψφ
4 3 adantr xyxRyφxy|φVxyxRyψφ
5 ssopab2 xyxRyψφxy|xRyψxy|φ
6 4 5 syl xyxRyφxy|φVxy|xRyψxy|φ
7 1 6 ssexd xyxRyφxy|φVxy|xRyψV