Metamath Proof Explorer


Theorem eliniseg2

Description: Eliminate the class existence constraint in eliniseg . (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by Mario Carneiro, 17-Nov-2015)

Ref Expression
Assertion eliniseg2 Rel A C A -1 B C A B

Proof

Step Hyp Ref Expression
1 relcnv Rel A -1
2 elrelimasn Rel A -1 C A -1 B B A -1 C
3 1 2 ax-mp C A -1 B B A -1 C
4 relbrcnvg Rel A B A -1 C C A B
5 3 4 syl5bb Rel A C A -1 B C A B