Theorem dfmember2

Description: Alternate definition of the membership equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021)

	Ref	Expression
Assertion	dfmember2	⊢ ( MembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfmember	⊢ ( MembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴 )
2		dferALTV2	⊢ ( ∼ 𝐴 ErALTV 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
3	1 2	bitri	⊢ ( MembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )