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 e. ( `' A " { B } ) <-> C A B ) )

Proof

Step Hyp Ref Expression
1 relcnv
 |-  Rel `' A
2 elrelimasn
 |-  ( Rel `' A -> ( C e. ( `' A " { B } ) <-> B `' A C ) )
3 1 2 ax-mp
 |-  ( C e. ( `' A " { B } ) <-> B `' A C )
4 relbrcnvg
 |-  ( Rel A -> ( B `' A C <-> C A B ) )
5 3 4 syl5bb
 |-  ( Rel A -> ( C e. ( `' A " { B } ) <-> C A B ) )