Theorem elecg

Description: Membership in an equivalence class. Theorem 72 of Suppes p. 82. (Contributed by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	elecg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elimasng	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ ( 𝑅 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ 𝑅 ) )
2	1	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∈ ( 𝑅 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ 𝑅 ) )
3		df-ec	⊢ [ 𝐵 ] 𝑅 = ( 𝑅 “ { 𝐵 } )
4	3	eleq2i	⊢ ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐴 ∈ ( 𝑅 “ { 𝐵 } ) )
5		df-br	⊢ ( 𝐵 𝑅 𝐴 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ 𝑅 )
6	2 4 5	3bitr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝐴 ) )