Metamath Proof Explorer

Theorem extep

Description: Property of epsilon relation, see also extid , extssr and the comment of df-ssr . (Contributed by Peter Mazsa, 10-Jul-2019)

Ref Expression
Assertion extep 
|- ( ( A e. V /\ B e. W ) -> ( [ A ] `' _E = [ B ] `' _E <-> A = B ) )

Proof

Step Hyp Ref Expression
1 eccnvep 
 |-  ( A e. V -> [ A ] `' _E = A )
2 eccnvep 
 |-  ( B e. W -> [ B ] `' _E = B )
3 1 2 eqeqan12d 
 |-  ( ( A e. V /\ B e. W ) -> ( [ A ] `' _E = [ B ] `' _E <-> A = B ) )