Description: One times a cardinal number. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xp1en | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 1o ) ≈ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 | ⊢ 1o = { ∅ } | |
2 | 1 | xpeq2i | ⊢ ( 𝐴 × 1o ) = ( 𝐴 × { ∅ } ) |
3 | 0ex | ⊢ ∅ ∈ V | |
4 | xpsneng | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∅ ∈ V ) → ( 𝐴 × { ∅ } ) ≈ 𝐴 ) | |
5 | 3 4 | mpan2 | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × { ∅ } ) ≈ 𝐴 ) |
6 | 2 5 | eqbrtrid | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 1o ) ≈ 𝐴 ) |