Metamath Proof Explorer

Theorem 1cosscnvepresex

Description: Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021)

Ref Expression
Assertion 1cosscnvepresex 
|- ( A e. V -> ,~ ( `' _E |` A ) e. _V )

Proof

Step Hyp Ref Expression
1 cnvepresex 
 |-  ( A e. V -> ( `' _E |` A ) e. _V )
2 cossex 
 |-  ( ( `' _E |` A ) e. _V -> ,~ ( `' _E |` A ) e. _V )
3 1 2 syl 
 |-  ( A e. V -> ,~ ( `' _E |` A ) e. _V )