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

Ref | Expression | ||
---|---|---|---|

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

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | elimasng | ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ ( 𝑅 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ 𝑅 ) ) | |

2 | 1 | ancoms | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∈ ( 𝑅 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ 𝑅 ) ) |

3 | df-ec | ⊢ [ 𝐵 ] 𝑅 = ( 𝑅 “ { 𝐵 } ) | |

4 | 3 | eleq2i | ⊢ ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐴 ∈ ( 𝑅 “ { 𝐵 } ) ) |

5 | df-br | ⊢ ( 𝐵 𝑅 𝐴 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ 𝑅 ) | |

6 | 2 4 5 | 3bitr4g | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝐴 ) ) |