| Intuitionistic Logic Explorer | 
      
      
      < Previous  
      Next >
      
       Nearby theorems  | 
  ||
| Mirrors > Home > ILE Home > Th. List > eleq1 | GIF version | ||
| Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) | 
| Ref | Expression | 
|---|---|
| eleq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eqeq2 2206 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵)) | |
| 2 | 1 | anbi1d 465 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))) | 
| 3 | 2 | exbidv 1839 | . 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))) | 
| 4 | df-clel 2192 | . 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
| 5 | df-clel 2192 | . 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
| 6 | 3, 4, 5 | 3bitr4g 223 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | 
| Copyright terms: Public domain | W3C validator |