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 ) ) |
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 ) ) |