Theorem dfcomember

Description: Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022)

	Ref	Expression
Assertion	dfcomember	⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-comember	⊢ ( CoMembEr 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 )
2		df-coels	⊢ ∼ 𝐴 = ≀ ( ◡ E ↾ 𝐴 )
3	2	erALTVeq1i	⊢ ( ∼ 𝐴 ErALTV 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 )
4	1 3	bitr4i	⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴 )