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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ◡ E = [ 𝐵 ] ◡ E ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eccnvep	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ◡ E = 𝐴 )
2		eccnvep	⊢ ( 𝐵 ∈ 𝑊 → [ 𝐵 ] ◡ E = 𝐵 )
3	1 2	eqeqan12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ◡ E = [ 𝐵 ] ◡ E ↔ 𝐴 = 𝐵 ) )