|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > elrnmpt | Structured version Visualization version GIF version | ||
| Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.) | 
| Ref | Expression | 
|---|---|
| rnmpt.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | 
| Ref | Expression | 
|---|---|
| elrnmpt | ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eqeq1 2740 | . . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐵 ↔ 𝐶 = 𝐵)) | |
| 2 | 1 | rexbidv 3178 | . 2 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | 
| 3 | rnmpt.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
| 4 | 3 | rnmpt 5967 | . 2 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} | 
| 5 | 2, 4 | elab2g 3679 | 1 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | 
| Copyright terms: Public domain | W3C validator |