Metamath Proof Explorer


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 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐵 ∈ [ 𝐴 ] 𝑅𝐴 𝑅 𝐵 ) )