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 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elimasng | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∈ ( 𝑅 “ { 𝐴 } ) ↔ 〈 𝐴 , 𝐵 〉 ∈ 𝑅 ) ) | |
2 | df-ec | ⊢ [ 𝐴 ] 𝑅 = ( 𝑅 “ { 𝐴 } ) | |
3 | 2 | eleq2i | ⊢ ( 𝐵 ∈ [ 𝐴 ] 𝑅 ↔ 𝐵 ∈ ( 𝑅 “ { 𝐴 } ) ) |
4 | df-br | ⊢ ( 𝐴 𝑅 𝐵 ↔ 〈 𝐴 , 𝐵 〉 ∈ 𝑅 ) | |
5 | 1 3 4 | 3bitr4g | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝐵 ) ) |