This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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