Metamath Proof Explorer


Theorem supex2g

Description: Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion supex2g A C sup B A R V

Proof

Step Hyp Ref Expression
1 df-sup sup B A R = x A | y B ¬ x R y y A y R x z B y R z
2 rabexg A C x A | y B ¬ x R y y A y R x z B y R z V
3 2 uniexd A C x A | y B ¬ x R y y A y R x z B y R z V
4 1 3 eqeltrid A C sup B A R V