Description: The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Hypothesis | f1dom.1 | ⊢ 𝐵 ∈ V | |
Assertion | f1dom | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐴 ≼ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1dom.1 | ⊢ 𝐵 ∈ V | |
2 | f1domg | ⊢ ( 𝐵 ∈ V → ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐴 ≼ 𝐵 ) ) | |
3 | 1 2 | ax-mp | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐴 ≼ 𝐵 ) |