Theorem elecALTV

Description: Elementhood in the R -coset of A . Theorem 72 of Suppes p. 82. (I think we should replace elecg with this original form of Suppes. Peter Mazsa). (Contributed by Mario Carneiro, 9-Jul-2014)

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

Proof

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